diff -r b94cd208f073 -r 7ac22e5a05d7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 15 10:15:13 1998 +0200
+++ b/src/HOL/Set.thy	Wed Jul 15 10:58:44 1998 +0200
@@ -71,6 +71,8 @@
   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
 
+  disjoint      :: 'a set => 'a set => bool
+
 translations
   "range f"     == "f``UNIV"
   "x ~: y"      == "~ (x : y)"
@@ -87,6 +89,7 @@
   "? x:A. P"    == "Bex A (%x. P)"
   "ALL x:A. P"  => "Ball A (%x. P)"
   "EX x:A. P"   => "Bex A (%x. P)"
+  "disjoint A B" == "A <= Compl B"
 
 syntax ("" output)
   "_setle"      :: ['a set, 'a set] => bool           ("op <=")