--- a/src/HOL/Set.ML Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Set.ML Mon Mar 04 14:37:33 1996 +0100
@@ -257,7 +257,6 @@
qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
(fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
-
(*** The empty set -- {} ***)
qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
@@ -320,6 +319,13 @@
by (rtac singletonI 1);
qed "singleton_inject";
+
+(*** UNIV - The universal set ***)
+
+qed_goal "subset_UNIV" Set.thy "A <= UNIV"
+ (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
+
+
(*** Unions of families -- UNION x:A. B(x) is Union(B``A) ***)
(*The order of the premises presupposes that A is rigid; b may be flexible*)