disjoint
authornipkow
Wed, 15 Jul 1998 11:15:57 +0200
changeset 5145 963aff0818c2
parent 5144 7ac22e5a05d7
child 5146 1ea751ae62b2
disjoint
NEWS
--- 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);