# HG changeset patch # User ballarin # Date 1529434952 -7200 # Node ID aad109fde9ec1df5c01f92c8345fd7c4082a8ab1 # Parent ae42b0f6885d9988c1513958fcac78416629d1d1 In interpretation commands, clarify what to do with definitions immediately subject to rewriting. diff -r ae42b0f6885d -r aad109fde9ec NEWS --- a/NEWS Tue Jun 19 12:14:31 2018 +0100 +++ b/NEWS Tue Jun 19 21:02:32 2018 +0200 @@ -195,7 +195,8 @@ * Rewrites clauses (keyword 'rewrites') were moved into the locale expression syntax, where they are part of locale instances. In interpretation commands rewrites clauses now need to occur before 'for' -and 'defines'. Minor INCOMPATIBILITY. +and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to +rewriting may need to be pulled up into the surrounding theory. * For 'rewrites' clauses, if activating a locale instance fails, fall back to reading the clause first. This helps avoid qualification of