summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 10 Sep 1998 18:07:06 +0200 | |

changeset 5475 | 410172655d64 |

parent 5474 | a2109bb8ce2b |

child 5476 | 1c09934fe445 |

equals0D

--- 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)