# HG changeset patch
# User paulson
# Date 919675172 -3600
# Node ID 694c9c1910e82d5eb5b408410b44632bd863c176
# Parent  61904a3eafaa8e9b9cd0c35f178bc89a5d9e4449
new theorems Pow_0 and Pow_insert; renamed other Pow theorems

diff -r 61904a3eafaa -r 694c9c1910e8 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Feb 22 10:16:59 1999 +0100
+++ b/src/ZF/equalities.ML	Mon Feb 22 10:19:32 1999 +0100
@@ -555,6 +555,18 @@
 
 (** Pow **)
 
+Goal "Pow(0) = {0}";
+by (Blast_tac 1);
+qed "Pow_0";
+
+Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}";
+br equalityI 1;
+by Safe_tac;
+by (etac swap 1);
+by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);
+by (ALLGOALS Blast_tac);
+qed "Pow_insert";
+
 Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
 by (Blast_tac 1);
 qed "Un_Pow_subset";
@@ -573,13 +585,13 @@
 
 Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
 by (Blast_tac 1);
-qed "Int_Pow_eq";
+qed "Pow_Int_eq";
 
-Goal "x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+Goal "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
 by (Blast_tac 1);
-qed "INT_Pow_subset";
+qed "Pow_INT_eq";
 
-Addsimps [Union_Pow_eq, Int_Pow_eq];
+Addsimps [Pow_0, Union_Pow_eq, Pow_Int_eq];
 
 (** RepFun **)