Improved the proof of Problem 38
authorpaulson
Mon, 19 Aug 1996 11:22:16 +0200
changeset 1915 7cd464e3e3c6
parent 1914 86b095835de9
child 1916 43521f79f016
Improved the proof of Problem 38
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";