author | wenzelm |
Tue, 04 Aug 1998 09:22:07 +0200 | |
changeset 5236 | 0cec0b591d4c |
parent 5235 | c404f25c58e8 |
child 5237 | aebc63048f2d |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- 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)"