--- a/NEWS Fri Jun 29 14:19:52 2018 +0200
+++ b/NEWS Fri Jun 29 15:54:41 2018 +0200
@@ -19,6 +19,11 @@
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+* Global facts need to be closed: no free variables, no hypotheses, no
+pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
+allowed via "declare [[pending_shyps]]" in the global theory context,
+but it should be reset to false afterwards.
+
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle