# HG changeset patch
# User paulson
# Date 840446536 -7200
# Node ID 7cd464e3e3c65720884a7a684fc1e0ef19969df2
# Parent  86b095835de9e10bcd4c3f2d4988263a9ed82d29
Improved the proof of Problem 38

diff -r 86b095835de9 -r 7cd464e3e3c6 src/FOL/ex/cla.ML
--- 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";