NEWS
changeset 68540 000a0e062529
parent 68523 ccacc84e0251
child 68541 12b4b3bc585d
     1.1 --- a/NEWS	Fri Jun 29 14:19:52 2018 +0200
     1.2 +++ b/NEWS	Fri Jun 29 15:54:41 2018 +0200
     1.3 @@ -19,6 +19,11 @@
     1.4  FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
     1.5  formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
     1.6  
     1.7 +* Global facts need to be closed: no free variables, no hypotheses, no
     1.8 +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
     1.9 +allowed via "declare [[pending_shyps]]" in the global theory context,
    1.10 +but it should be reset to false afterwards.
    1.11 +
    1.12  * Marginal comments need to be written exclusively in the new-style form
    1.13  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.14  supported. INCOMPATIBILITY, use the command-line tool "isabelle