--- a/NEWS Wed Jul 15 10:58:44 1998 +0200
+++ b/NEWS Wed Jul 15 11:15:57 1998 +0200
@@ -1,4 +1,3 @@
-
Isabelle NEWS -- history of user-visible changes
================================================
@@ -144,6 +143,9 @@
* 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);