disjointness
authorpaulson
Thu Aug 06 10:50:44 1998 +0200 (1998-08-06)
changeset 526741a01176b9de
parent 5266 1d11c7e4b999
child 5268 59ef39008514
disjointness
NEWS
     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,...);