1.1 --- a/src/HOL/Set.thy	Tue Aug 04 09:21:44 1998 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Aug 04 09:22:07 1998 +0200
     1.3 @@ -89,7 +89,6 @@
     1.4    "? x:A. P"    == "Bex A (%x. P)"
     1.5    "ALL x:A. P"  => "Ball A (%x. P)"
     1.6    "EX x:A. P"   => "Bex A (%x. P)"
     1.7 -  "disjoint A B" == "A <= Compl B"
     1.8  
     1.9  syntax ("" output)
    1.10    "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    1.11 @@ -126,6 +125,7 @@
    1.12  translations
    1.13    "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
    1.14    "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
    1.15 +  "disjoint A B" == "_setle A (Compl B)"
    1.16  
    1.17  
    1.18