*** General ***
* 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'.
This refers to Isabelle/de610e8df459. Following the principle that we
share with the GHC guys "we obsessively refactor while adding new code,
keeping the code base as fresh as possible", I have made some cleanups
before adding yet another toplevel theorem alias. So the resulting
situation is a bit simpler than before.
Internally there is only the one Thm.theoremK tag left over -- and it is
actually legacy. See also fa4ebbd350ae.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
