changeset 5310 | 3e14d6d66dab |
parent 5219 | 924359415f09 |
child 6260 | a8010d459ef7 |
--- a/src/FOL/ROOT.ML Thu Aug 13 17:28:52 1998 +0200 +++ b/src/FOL/ROOT.ML Thu Aug 13 17:29:18 1998 +0200 @@ -55,7 +55,7 @@ qed_goal "ex1_functional" FOL.thy "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" - (fn _ => [ (deepen_tac FOL_cs 0 1) ]); + (fn _ => [ (Blast_tac 1) ]); print_depth 8;