src/ZF/ex/misc.ML

--- a/src/ZF/ex/misc.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/misc.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -145,9 +145,7 @@
 \    : bij(Pow(A+B), Pow(A)*Pow(B))";
 by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
     lam_bijective 1);
-by (TRYALL (etac SigmaE));
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (!claset addSIs [equalityI])));
+by (Auto_tac());
 val Pow_bij = result();
 
 writeln"Reached end of file.";