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

[Fabian Huch]

Hi,


unnamed facts at the top level of a theory (i.e., unnamed lemmas or 
theorems) don't work smoothly with the rest of Isabelle.

For instance:

- they appear nowhere in the theory exports (naively, one could think 
they appear as literal facts)

- unused_thms ignores them and thus will report facts that are only used 
by unnamed facts as unused


I see three possible ways to do improve this:

1. Make it explicit that unnamed top level facts are for "demonstration 
purposes only" and should otherwise not be used
     (for instance by creating a distinct command for unnamed 
lemmas/theorems and requiring a name otherwise)

2. Make unnamed top level facts accessible as theory facts, and improve 
the tools to use them properly

3. Keep the handling for unnamed facts as is, but tweak the tools a bit 
(for instance, assume [simp] lemmas always used in unused_thms)


Which route should we go?


Fabian