src/FOL/ex/Classical.thy

     (\<exists>v. C(v) &                                                        
           (\<forall>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)))))  
    -->                   
    ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (tactic{*Blast.depth_tac @{claset} 12 1*})
+by (blast 12)
    --{*Needed because the search for depths below 12 is very slow*}
 
 
 text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*}
 lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->