# HG changeset patch
# User nipkow
# Date 900494157 -7200
# Node ID 963aff0818c2592ae7cecf2c6356f77c7025391b
# Parent  7ac22e5a05d75e0f0356f27ce78e98a4570e0f11
disjoint

diff -r 7ac22e5a05d7 -r 963aff0818c2 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);