NEWS
changeset 68665 5820f0f379ae
parent 68647 f0d98441eff5
child 68681 14167c321d22
     1.1 --- a/NEWS	Wed Jul 18 20:51:23 2018 +0200
     1.2 +++ b/NEWS	Fri Jul 20 03:14:44 2018 +0200
     1.3 @@ -22,6 +22,12 @@
     1.4  * Global facts need to be closed: no free variables and no hypotheses.
     1.5  Rare INCOMPATIBILITY.
     1.6  
     1.7 +* Facts stemming from locale interpretation are subject to lazy
     1.8 +evaluation for improved performance. Rare INCOMPATIBILITY: errors
     1.9 +stemming from interpretation morphisms might be deferred and thus
    1.10 +difficult to locate; enable system option "strict_facts" temporarily to
    1.11 +avoid this.
    1.12 +
    1.13  * Marginal comments need to be written exclusively in the new-style form
    1.14  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.15  supported. INCOMPATIBILITY, use the command-line tool "isabelle