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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
