src/ZF/ex/misc.ML

--- a/src/ZF/ex/misc.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/ex/misc.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -155,7 +155,8 @@
 \    : 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 (Auto_tac());
-val Pow_bij = result();
+(*Auto_tac no longer proves it*)
+by (REPEAT (fast_tac (claset() addss (simpset())) 1));
+qed "Pow_bij";
 
 writeln"Reached end of file.";