new theorem Pow_UNIV
authorpaulson
Wed Dec 02 15:53:22 1998 +0100 (1998-12-02)
changeset 600791070f559b4d
parent 6006 d2e271b8d651
child 6008 d0e9b1619468
new theorem Pow_UNIV
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Wed Dec 02 15:53:05 1998 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Dec 02 15:53:22 1998 +0100
     1.3 @@ -776,6 +776,11 @@
     1.4  by (ALLGOALS Blast_tac);
     1.5  qed "Pow_insert";
     1.6  
     1.7 +Goal "Pow UNIV = UNIV";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Pow_UNIV";
    1.10 +Addsimps [Pow_UNIV];
    1.11 +
    1.12  (** for datatypes **)
    1.13  Goal "f x ~= f y ==> x ~= y";
    1.14  by (Fast_tac 1);