author | paulson |

Thu Aug 06 10:50:44 1998 +0200 (1998-08-06) | |

changeset 5267 | 41a01176b9de |

parent 5266 | 1d11c7e4b999 |

child 5268 | 59ef39008514 |

disjointness

1.1 --- a/NEWS Thu Aug 06 10:47:13 1998 +0200 1.2 +++ b/NEWS Thu Aug 06 10:50:44 1998 +0200 1.3 @@ -93,7 +93,7 @@ 1.4 *** HOL *** 1.5 1.6 * HOL/inductive package reorganized and improved: now supports mutual 1.7 -definitions such as: 1.8 +definitions such as 1.9 1.10 inductive EVEN ODD 1.11 intrs 1.12 @@ -111,7 +111,7 @@ 1.13 1.14 1.15 * HOL/datatype package re-implemented and greatly improved: now 1.16 -supports mutually recursive datatypes such as: 1.17 +supports mutually recursive datatypes such as 1.18 1.19 datatype 1.20 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) 1.21 @@ -123,7 +123,7 @@ 1.22 | AND ('a bexp) ('a bexp) 1.23 | OR ('a bexp) ('a bexp) 1.24 1.25 -as well as indirectly recursive datatypes such as: 1.26 +as well as indirectly recursive datatypes such as 1.27 1.28 datatype 1.29 ('a, 'b) term = Var 'a 1.30 @@ -185,6 +185,8 @@ 1.31 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which 1.32 makes more sense); 1.33 1.34 +* HOL/Set INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name was misleading); 1.35 + 1.36 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1 1.37 to 'converse' from 'inverse' (for compatibility with ZF and some 1.38 literature); 1.39 @@ -210,9 +212,6 @@ 1.40 * HOL/Relation: renamed the relational operator r^-1 "converse" 1.41 instead of "inverse"; 1.42 1.43 -* HOL/Set: added the predicate "disjoint A B" that stands for "A <= Compl B". 1.44 - This is much better than "A Int B = {}" for Fast/Blast_tac. 1.45 - 1.46 * directory HOL/Real: a construction of the reals using Dedekind cuts 1.47 (not included by default); 1.48 1.49 @@ -226,6 +225,11 @@ 1.50 1.51 * theory Main includes everything; 1.52 1.53 +* ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name 1.54 + was misleading). The rule and 'sym RS equals0E' are now in the default 1.55 + claset, giving automatic disjointness reasoning but breaking a few old 1.56 + proofs. 1.57 + 1.58 * ZF/Update: new theory of function updates 1.59 with default rewrite rule f(x:=y) ` z = if(z=x, y, f`z) 1.60 may also be iterated as in f(a:=b,c:=d,...);