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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
