changeset 5236 | 0cec0b591d4c |
parent 5144 | 7ac22e5a05d7 |
child 5254 | a275d0a3dc08 |
--- a/src/HOL/Set.thy Tue Aug 04 09:21:44 1998 +0200 +++ b/src/HOL/Set.thy Tue Aug 04 09:22:07 1998 +0200 @@ -89,7 +89,6 @@ "? x:A. P" == "Bex A (%x. P)" "ALL x:A. P" => "Ball A (%x. P)" "EX x:A. P" => "Bex A (%x. P)" - "disjoint A B" == "A <= Compl B" syntax ("" output) "_setle" :: ['a set, 'a set] => bool ("op <=") @@ -126,6 +125,7 @@ translations "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool" "op \\<subset>" => "op < :: [_ set, _ set] => bool" + "disjoint A B" == "_setle A (Compl B)"