--- a/Set.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Set.ML Thu Aug 25 11:01:45 1994 +0200
@@ -434,3 +434,14 @@
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
val InterE = result();
+
+(*** Powerset ***)
+
+val PowI = prove_goalw Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
+ (fn _ => [ (etac CollectI 1) ]);
+
+val PowD = prove_goalw Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B"
+ (fn _=> [ (etac CollectD 1) ]);
+
+val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
+val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)