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

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


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


More information about the isabelle-dev mailing list