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

[Tobias Nipkow]

I gave some good reasons. In fact such unnamed lemmas can be a downright pain, eg

lemma [simp]: "..."

Can you give a good reason to keep them other than "we always did it like that"? 
I mean a real reason like "they are required because" or "it would break X".

Can you explain why you think it will take years to add names to existing 
unnamed thms? Not that it matters that much if we agree that it should be changed.

Tobias

On 05/11/2020 16:55, Makarius wrote:
> On 05/11/2020 16:52, Tobias Nipkow wrote:
>> 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.
> 
> Such a profound change of how Isabelle works needs good justifications. And
> afterwards it usually takes years to get such a change through.
> 
> 
> 	Makarius
> 

-------------- 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/cfea6028/attachment.bin>