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

author | paulson |

Thu, 06 Aug 1998 10:50:44 +0200 | |

changeset 5267 | 41a01176b9de |

parent 5266 | 1d11c7e4b999 |

child 5268 | 59ef39008514 |

disjointness

--- a/NEWS Thu Aug 06 10:47:13 1998 +0200 +++ b/NEWS Thu Aug 06 10:50:44 1998 +0200 @@ -93,7 +93,7 @@ *** HOL *** * HOL/inductive package reorganized and improved: now supports mutual -definitions such as: +definitions such as inductive EVEN ODD intrs @@ -111,7 +111,7 @@ * HOL/datatype package re-implemented and greatly improved: now -supports mutually recursive datatypes such as: +supports mutually recursive datatypes such as datatype 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) @@ -123,7 +123,7 @@ | AND ('a bexp) ('a bexp) | OR ('a bexp) ('a bexp) -as well as indirectly recursive datatypes such as: +as well as indirectly recursive datatypes such as datatype ('a, 'b) term = Var 'a @@ -185,6 +185,8 @@ * 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/Relation INCOMPATIBILITY: renamed the relational operator r^-1 to 'converse' from 'inverse' (for compatibility with ZF and some literature); @@ -210,9 +212,6 @@ * HOL/Relation: renamed the relational operator r^-1 "converse" instead of "inverse"; -* HOL/Set: added the predicate "disjoint A B" that stands for "A <= Compl B". - This is much better than "A Int B = {}" for Fast/Blast_tac. - * directory HOL/Real: a construction of the reals using Dedekind cuts (not included by default); @@ -226,6 +225,11 @@ * theory Main includes everything; +* 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/Update: new theory of function updates with default rewrite rule f(x:=y) ` z = if(z=x, y, f`z) may also be iterated as in f(a:=b,c:=d,...);