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