new theorem Pow_UNIV

--- a/src/HOL/equalities.ML	Wed Dec 02 15:53:05 1998 +0100
+++ b/src/HOL/equalities.ML	Wed Dec 02 15:53:22 1998 +0100
@@ -776,6 +776,11 @@
 by (ALLGOALS Blast_tac);
 qed "Pow_insert";
 
+Goal "Pow UNIV = UNIV";
+by (Blast_tac 1);
+qed "Pow_UNIV";
+Addsimps [Pow_UNIV];
+
 (** for datatypes **)
 Goal "f x ~= f y ==> x ~= y";
 by (Fast_tac 1);