NEWS
changeset 67764 0f8cb5568b63
parent 67741 d5a7f2c54655
child 67830 4f992daf4707
     1.1 --- a/NEWS	Sat Mar 03 22:33:25 2018 +0100
     1.2 +++ b/NEWS	Sun Mar 04 12:22:48 2018 +0100
     1.3 @@ -176,14 +176,14 @@
     1.4  (e.g. use 'find_theorems' or 'try' to figure this out).
     1.5  
     1.6  * Rewrites clauses (keyword 'rewrites') were moved into the locale
     1.7 -expression syntax, where they are part of locale instances.  Keyword
     1.8 -'for' now needs to occur after, not before 'rewrites'.
     1.9 -Minor INCOMPATIBILITY.
    1.10 -
    1.11 -* For rewrites clauses in locale expressions, if activating a locale
    1.12 -instance fails, fall back to reading the clause first.  This helps
    1.13 -avoiding qualified locale instances where the qualifier's sole purpose
    1.14 -is avoiding duplicate constant declarations.
    1.15 +expression syntax, where they are part of locale instances.  In
    1.16 +interpretation commands rewrites clauses now need to occur before
    1.17 +'for' and 'defines'.  Minor INCOMPATIBILITY.
    1.18 +
    1.19 +* For rewrites clauses, if activating a locale instance fails, fall
    1.20 +back to reading the clause first.  This helps avoid qualification of
    1.21 +locale instances where the qualifier's sole purpose is avoiding
    1.22 +duplicate constant declarations.
    1.23  
    1.24  
    1.25  *** Pure ***