changeset 42789 | 3a84b6947932 |
parent 36319 | 8feb2c4bef1a |
child 51717 | 9e7d1c139569 |
--- a/src/FOL/ex/Classical.thy Fri May 13 14:26:51 2011 +0200 +++ b/src/FOL/ex/Classical.thy Fri May 13 14:39:55 2011 +0200 @@ -436,7 +436,7 @@ ((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*}