| changeset 6007 | 91070f559b4d |
| parent 5999 | 84fe61a08c17 |
| child 6283 | e3096df44326 |
--- 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);