# HG changeset patch
# User paulson
# Date 971771248 -7200
# Node ID c8726d4ee89a64e2717eb78f0e66855946507414
# Parent  08083bd2a64d99759543572ef1d898851c1e3de7
tidied some awkward proofs

diff -r 08083bd2a64d -r c8726d4ee89a src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Oct 17 10:26:07 2000 +0200
+++ b/src/HOL/equalities.ML	Tue Oct 17 10:27:28 2000 +0200
@@ -843,17 +843,11 @@
 Addsimps [Pow_empty];
 
 Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
-by Safe_tac;
-by (etac swap 1);
-by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
 qed "Pow_insert";
 
 Goal "Pow (- A) = {-B |B. A: Pow B}";
-by Safe_tac;
-by (Blast_tac 2);
-by (res_inst_tac [("x", "-x")] exI 1);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1);
 qed "Pow_Compl";
 
 Goal "Pow UNIV = UNIV";