Email Gateway (Aug 23 2022 at 09:04): Email Gateway (Aug 23 2022 at 09:04):From: Lars-Henrik Eriksson <lhe@it.uu.se>
The attached theory causes a sledgehammer error in Isabelle 2020.
The theory is as small as I have been able to make it. Seemingly unrelated things like the datatype declaration, the function p and even the locale names (!) matter.
Even more odd is that editing the theory in Isabelle and then undoing the edits sometimes causes the error to go away. Loading the theory in a fresh instance of Isabelle always triggers the error, however.
Lars-Henrik
Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden
E-mail: lhe@it.uu.se, Web: http://www.it.uu.se/katalog/lhe?lang=en
Phone: +46 18 471 10 57, Mobile: +46 705-36 39 16, Fax: +46 18 51 19 25
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Z3bug.thy
Email Gateway (Aug 23 2022 at 09:04):From: Lars-Henrik Eriksson <lhe@it.uu.se>
5 maj 2020 kl. 18:05 skrev Lars-Henrik Eriksson <lhe@it.uu.se>:
The attached theory causes a sledgehammer error in Isabelle 2020.
I should add that I'm running Isabelle 2020 on a MacBook Pro with 4 cores and 16 GB memory under MacOSX 10.13.6.
Lars-Henrik
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Last updated: Apr 23 2024 at 16:19 UTC