# HG changeset patch
# User lcp
# Date 756478692 -3600
# Node ID 0f0ff91b07f627df8ca9913de425b90affb60c4c
# Parent  7c7179e687b21d2ba21a56d4eec6a96032cd0f34
new section for equality properties

diff -r 7c7179e687b2 -r 0f0ff91b07f6 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Tue Dec 14 14:02:52 1993 +0100
+++ b/src/ZF/equalities.ML	Tue Dec 21 13:58:12 1993 +0100
@@ -322,3 +322,28 @@
 by (fast_tac eq_cs 1);
 val converse_diff = result();
 
+(** Pow **)
+
+goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
+by (fast_tac upair_cs 1);
+val Un_Pow_subset = result();
+
+goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
+by (fast_tac upair_cs 1);
+val UN_Pow_subset = result();
+
+goal ZF.thy "A <= Pow(Union(A))";
+by (fast_tac upair_cs 1);
+val subset_Pow_Union = result();
+
+goal ZF.thy "Union(Pow(A)) = A";
+by (fast_tac eq_cs 1);
+val Union_Pow_eq = result();
+
+goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";
+by (fast_tac eq_cs 1);
+val Int_Pow_eq = result();
+
+goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+by (fast_tac eq_cs 1);
+val INT_Pow_subset = result();