src/FOL/ex/cla.ML

     "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
 \            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
 \    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
 \            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
 \             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
-by (fast_tac FOL_cs 1);
+by (deepen_tac FOL_cs 0 1);  (*beats fast_tac!*)
 result();
 
 writeln"Problem 39";
 goal FOL.thy "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
 by (fast_tac FOL_cs 1);