diff -r a2109bb8ce2b -r 410172655d64 NEWS
--- a/NEWS	Thu Sep 10 18:06:39 1998 +0200
+++ b/NEWS	Thu Sep 10 18:07:06 1998 +0200
@@ -198,7 +198,9 @@
 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
 makes more sense);
 
-* HOL/Set INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name was misleading);
+* HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
+  It and 'sym RS equals0D' are now in the default  claset, giving automatic
+  disjointness reasoning but breaking a few old proofs.
 
 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
 to 'converse' from 'inverse' (for compatibility with ZF and some
@@ -245,10 +247,9 @@
 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
   only the theorems proved on ZF.ML;
 
-* ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
-  was misleading).  The rule and 'sym RS equals0E' are now in the default
-  claset, giving automatic disjointness reasoning but breaking a few old 
-  proofs.
+* ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
+  It and 'sym RS equals0D' are now in the default  claset, giving automatic
+  disjointness reasoning but breaking a few old proofs.
 
 * ZF/Update: new theory of function updates
     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)