# 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"
``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.
* Toplevel theorem statement 'proposition' is another alias for
'theorem'.
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*