Re: [isabelle] Isabelle2016-RC0 - output says "theorem" when I called it a "lemma"
On Fri, 15 Jan 2016, Eugene W. Stark wrote:
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?
Neither. It is just a consequence of how certain things work.
When you say 'definition' you get a report about internal "constants"
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
* Toplevel theorem statement 'proposition' is another alias for
This archive was generated by a fusion of
Pipermail (Mailman edition) and