In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
authorballarin
Tue Jun 19 21:02:32 2018 +0200 (18 months ago)
changeset 68469aad109fde9ec
parent 68468 ae42b0f6885d
child 68471 409ed528aad4
In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
NEWS
     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