src/HOL/Set.thy
changeset 5254 a275d0a3dc08
parent 5236 0cec0b591d4c
child 5492 d9fc3457554e
     1.1 --- a/src/HOL/Set.thy	Wed Aug 05 10:57:25 1998 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Aug 05 10:59:51 1998 +0200
     1.3 @@ -71,8 +71,6 @@
     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 @@ -125,7 +123,6 @@
    1.13  translations
    1.14    "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
    1.15    "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
    1.16 -  "disjoint A B" == "_setle A (Compl B)"
    1.17  
    1.18  
    1.19