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

[Makarius]

On 05/11/2020 16:39, Fabian Huch wrote:
> 
> unnamed facts at the top level of a theory (i.e., unnamed lemmas or theorems)
> don't work smoothly with the rest of Isabelle.
> 
> I see three possible ways to do improve this:

This behaviour it formal items with empty name binding is rather profound in
Isabelle.

The treatment of unnamed facts in particular is also fairly canonical
concerning our own standards.


Can you say what is wrong with this, and why it needs to be "improved"?


	Makarius