[isabelle-dev] Commands not in scope fail to cause errors
nipkow at in.tum.de
Fri Apr 10 09:03:29 CEST 2015
Something similar happens under 364b0512ce74 if the theory starts with a section
command followed by a lemma before the actual theory.
On 10/04/2015 08:56, Andreas Lochbihler wrote:
> Dear all,
> Today, I spent quite a while to figure out why in Isabelle/e936c2828bec one of
> my theories did not process completely in Isabelle/jEdit. Starting with a
> simps_of_case command, the rest of the theory stayed in the orange-ish color
> which indicates that this part had not yet been processed. poly kept running
> with full speed on all cores, but no progress was visible - not even one of the
> purple regions was visible.
> Ultimately, I found out that I had forgot to import the theory Simps_Case_Conv
> which defines the simps_of_case command (my base image already contains this
> theory, so the mark-up in jEdit was as usual and the theory goes through with
> Isabelle2014, as Isabelle2014 did not support local command scopes).
> Unfortunately, there was no error message at all or any other indication that an
> import is missing. I found this very confusing and suggest that this should be
> changed before the next release.
> I have attached an example theory which is supposed to be loaded with image
> HOL-Library. Without the import of Simps_Case_Conv, you should be able to
> observe the described behaviour.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev