--- a/NEWS Wed Jul 18 20:51:23 2018 +0200
+++ b/NEWS Fri Jul 20 03:14:44 2018 +0200
@@ -22,6 +22,12 @@
* Global facts need to be closed: no free variables and no hypotheses.
Rare INCOMPATIBILITY.
+* Facts stemming from locale interpretation are subject to lazy
+evaluation for improved performance. Rare INCOMPATIBILITY: errors
+stemming from interpretation morphisms might be deferred and thus
+difficult to locate; enable system option "strict_facts" temporarily to
+avoid this.
+
* 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