src/FOL/ex/cla.ML

 \   (EX v. C(v) &                                                       \
 \         (ALL y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &           \
 \                 ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b))))) \
 \  -->                  \
 \  ~ (EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z))))";
-by (Blast_tac 1);
+by (Blast.depth_tac (!claset) 12 1);
 result();
 
 
 (*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*)
 goal FOL.thy

 \  -->                                                            \
 \  (EX u. C(u) & (ALL y. (C(y) &  P(y,y) --> ~P(u,y)) &    \
 \                        (C(y) & ~P(y,y) --> P(u,y) & OO(u,b))))) \
 \  -->                                                            \
 \  ~ (EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z))))";
-by (Blast_tac 1);
+by (Blast.depth_tac(!claset) 7 1);
 result();
 
 (* Challenge found on info-hol *)
 goal FOL.thy
     "ALL x. EX v w. ALL y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))";

 
 (*Tue Mar  4 1997: loaded in 93s (on pochard, version 94-7) *)
 (*Tue Mar  4 1997: loaded in 89s (on pochard) *)
 (*Thu Apr  3 1997: loaded in 44s (on pochard)--using mostly Blast_tac*)
 (*Thu Apr  3 1997: loaded in 96s (on pochard)--addition of two Halting Probs*)
-
+(*Thu Apr  3 1997: loaded in 98s (on pochard)--using lim-1 for all haz rules*)
+