disjoint
authornipkow
Wed Jul 15 11:15:57 1998 +0200 (1998-07-15)
changeset 5145963aff0818c2
parent 5144 7ac22e5a05d7
child 5146 1ea751ae62b2
disjoint
NEWS
     1.1 --- a/NEWS	Wed Jul 15 10:58:44 1998 +0200
     1.2 +++ b/NEWS	Wed Jul 15 11:15:57 1998 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -144,6 +143,9 @@
     1.9  * HOL/Relation: renamed the relational operator r^-1 "converse"
    1.10  instead of "inverse";
    1.11  
    1.12 +* HOL/Set: added the predicate "disjoint A B" that stands for "A <= Compl B".
    1.13 +  This is much better than "A Int B = {}" for Fast/Blast_tac.
    1.14 +
    1.15  * directory HOL/Real: a construction of the reals using Dedekind cuts
    1.16  (not included by default);
    1.17