# HG changeset patch
# User paulson
# Date 902307591 -7200
# Node ID a275d0a3dc08f90867ddae0bbf10aeb6fd7b0863
# Parent  82a5ca6290aa37a192b2bb98ee821c1d91244ed0
Removal of "disjoint" translation

diff -r 82a5ca6290aa -r a275d0a3dc08 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)"