[isabelle-dev] NEWS: toplevel theorem statements

[Makarius]

*** 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