NEWS
changeset 5145 963aff0818c2
parent 5142 c56aa8b59dc0
child 5160 1ff6679144b9
     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