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

Makarius makarius at sketis.net
Thu Nov 5 16:55:55 CET 2020

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.


More information about the isabelle-dev mailing list