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

[Makarius]

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