author | lcp |
Thu, 24 Nov 1994 00:30:35 +0100 | |
changeset 731 | 435ff9ec4058 |
parent 730 | 15c822377c18 |
child 732 | 584b3475e859 |
src/FOL/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/FOL/ROOT.ML Wed Nov 23 11:45:56 1994 +0100 +++ b/src/FOL/ROOT.ML Thu Nov 24 00:30:35 1994 +0100 @@ -64,7 +64,7 @@ val ex1_functional = prove_goal FOL.thy "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" - (fn _ => [ (deepen_tac FOL_cs 1 1) ]); + (fn _ => [ (deepen_tac FOL_cs 0 1) ]); use "simpdata.ML";