NEWS
changeset 5475 410172655d64
parent 5428 5a6c4f666a25
child 5490 85855f65d0c6
     1.1 --- a/NEWS	Thu Sep 10 18:06:39 1998 +0200
     1.2 +++ b/NEWS	Thu Sep 10 18:07:06 1998 +0200
     1.3 @@ -198,7 +198,9 @@
     1.4  * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
     1.5  makes more sense);
     1.6  
     1.7 -* HOL/Set INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name was misleading);
     1.8 +* HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
     1.9 +  It and 'sym RS equals0D' are now in the default  claset, giving automatic
    1.10 +  disjointness reasoning but breaking a few old proofs.
    1.11  
    1.12  * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
    1.13  to 'converse' from 'inverse' (for compatibility with ZF and some
    1.14 @@ -245,10 +247,9 @@
    1.15  * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
    1.16    only the theorems proved on ZF.ML;
    1.17  
    1.18 -* ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
    1.19 -  was misleading).  The rule and 'sym RS equals0E' are now in the default
    1.20 -  claset, giving automatic disjointness reasoning but breaking a few old 
    1.21 -  proofs.
    1.22 +* ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
    1.23 +  It and 'sym RS equals0D' are now in the default  claset, giving automatic
    1.24 +  disjointness reasoning but breaking a few old proofs.
    1.25  
    1.26  * ZF/Update: new theory of function updates
    1.27      with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)