[isabelle-dev] Issues with unnamed top-level facts in Isabelle

[Tobias Nipkow]

I don't see any reason for allowing unnamed toplevel lemmas in a theory. Why 
should we continue to offer it? They are not useful, except for demo purposes, 
but then there are alternatives and it is also a bad idea to demo something that 
should be avoided.

Tobias

On 05/11/2020 16:48, Makarius wrote:
> On 05/11/2020 16:39, Fabian Huch wrote:
>>
>> unnamed facts at the top level of a theory (i.e., unnamed lemmas or theorems)
>> don't work smoothly with the rest of Isabelle.
>>
>> I see three possible ways to do improve this:
> 
> This behaviour it formal items with empty name binding is rather profound in
> Isabelle.
> 
> The treatment of unnamed facts in particular is also fairly canonical
> concerning our own standards.
> 
> 
> Can you say what is wrong with this, and why it needs to be "improved"?
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

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