summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)