src/FOL/ex/cla.ML
changeset 1915 7cd464e3e3c6
parent 1809 8cb50df49570
child 2469 b50b8c0eec01
--- a/src/FOL/ex/cla.ML	Mon Aug 19 11:20:37 1996 +0200
+++ b/src/FOL/ex/cla.ML	Mon Aug 19 11:22:16 1996 +0200
@@ -322,7 +322,7 @@
 \    (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";