Removal of "disjoint" translation
authorpaulson
Wed, 05 Aug 1998 10:59:51 +0200
changeset 5254 a275d0a3dc08
parent 5253 82a5ca6290aa
child 5255 e29e77ad7b91
Removal of "disjoint" translation
src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 05 10:57:25 1998 +0200
+++ b/src/HOL/Set.thy	Wed Aug 05 10:59:51 1998 +0200
@@ -71,8 +71,6 @@
   "*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)"
@@ -125,7 +123,6 @@
 translations
   "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
   "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
-  "disjoint A B" == "_setle A (Compl B)"