author | paulson |
Mon, 19 Aug 1996 11:22:16 +0200 | |
changeset 1915 | 7cd464e3e3c6 |
parent 1914 | 86b095835de9 |
child 1916 | 43521f79f016 |
src/FOL/ex/cla.ML | file | annotate | diff | comparison | revisions |
--- 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";