diff -r d9527f97246e -r 89669c58e506 Set.ML
--- 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) *)