In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
1.1 --- a/NEWS Tue Jun 19 12:14:31 2018 +0100
1.2 +++ b/NEWS Tue Jun 19 21:02:32 2018 +0200
1.3 @@ -195,7 +195,8 @@
1.4 * Rewrites clauses (keyword 'rewrites') were moved into the locale
1.5 expression syntax, where they are part of locale instances. In
1.6 interpretation commands rewrites clauses now need to occur before 'for'
1.7 -and 'defines'. Minor INCOMPATIBILITY.
1.8 +and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to
1.9 +rewriting may need to be pulled up into the surrounding theory.
1.10
1.11 * For 'rewrites' clauses, if activating a locale instance fails, fall
1.12 back to reading the clause first. This helps avoid qualification of