Email Gateway (Aug 22 2022 at 12:08): Email Gateway (Aug 22 2022 at 12:08):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Why does the output window report "theorem XXX" when the
cursor is at the end of the proof of something that I called
"lemma XXX"? Isabelle2015 didn't do this.
Is it intentional, or a bug?
- Gene Stark
Email Gateway (Aug 22 2022 at 12:08):From: Makarius <makarius@sketis.net>
Neither. It is just a consequence of how certain things work.
When you say 'definition' you get a report about internal "constants"
being defined.
When you say 'lemma', 'proposition', 'theorem' etc. you get a report about
an internal "theorem" definition in the end.
System output is often at a lower level than the primary text.
The internal distinction of different theorem "kinds" is a legacy feature
that has caused endless problems until today. Isabelle2016 makes one more
step to remove it.
For end-users the only relevant change is documented in NEWS:
Toplevel theorem statements have been simplified as follows:
theorems ~> lemmas
schematic_lemma ~> schematic_goal
schematic_theorem ~> schematic_goal
schematic_corollary ~> schematic_goal
Command-line tool "isabelle update_theorems" updates theory sources
accordingly.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC