src/HOL/Set.thy
changeset 5144 7ac22e5a05d7
parent 4761 1681b32dd134
child 5236 0cec0b591d4c
     1.1 --- a/src/HOL/Set.thy	Wed Jul 15 10:15:13 1998 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Jul 15 10:58:44 1998 +0200
     1.3 @@ -71,6 +71,8 @@
     1.4    "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
     1.5    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
     1.6  
     1.7 +  disjoint      :: 'a set => 'a set => bool
     1.8 +
     1.9  translations
    1.10    "range f"     == "f``UNIV"
    1.11    "x ~: y"      == "~ (x : y)"
    1.12 @@ -87,6 +89,7 @@
    1.13    "? x:A. P"    == "Bex A (%x. P)"
    1.14    "ALL x:A. P"  => "Ball A (%x. P)"
    1.15    "EX x:A. P"   => "Bex A (%x. P)"
    1.16 +  "disjoint A B" == "A <= Compl B"
    1.17  
    1.18  syntax ("" output)
    1.19    "_setle"      :: ['a set, 'a set] => bool           ("op <=")