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.