[isabelle-dev] Commands not in scope fail to cause errors

[Tobias Nipkow]

Something similar happens under 364b0512ce74 if the theory starts with a section 
command followed by a lemma before the actual theory.

Tobias

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.
>
> Best,
> Andreas
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150410/94126810/attachment.bin>