NEWS
changeset 68559 7aae213d9e69
parent 68548 a22540ac7052
child 68568 cf01d04e94d7
     1.1 --- a/NEWS	Sun Jul 01 12:37:24 2018 +0200
     1.2 +++ b/NEWS	Sun Jul 01 12:38:37 2018 +0200
     1.3 @@ -19,10 +19,8 @@
     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 +* Global facts need to be closed: no free variables and no hypotheses.
    1.12 +Rare INCOMPATIBILITY.
    1.13  
    1.14  * Marginal comments need to be written exclusively in the new-style form
    1.15  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer