# HG changeset patch
# User paulson
# Date 912610402 -3600
# Node ID 91070f559b4d7a596cec0684fe0eb5df0096980b
# Parent  d2e271b8d651a2e86434b4cde7e56944d37ea089
new theorem Pow_UNIV

diff -r d2e271b8d651 -r 91070f559b4d src/HOL/equalities.ML
--- 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);