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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
