changeset 9303 | f1ad1ed0d110 |
parent 9180 | 3bda56c0d70d |
child 9907 | 473a6604da94 |
--- a/src/ZF/equalities.ML Thu Jul 13 13:00:22 2000 +0200 +++ b/src/ZF/equalities.ML Thu Jul 13 13:02:20 2000 +0200 @@ -601,8 +601,7 @@ (** RepFun **) Goal "{f(x).x:A}=0 <-> A=0"; - (*blast_tac takes too long to find a good depth*) -by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1); +by (Blast_tac 1); qed "RepFun_eq_0_iff"; (** Collect **)