src/ZF/Nat.ML
changeset 2929 4eefc6c22d41
parent 2469 b50b8c0eec01
child 4091 771b1f6422a8
--- a/src/ZF/Nat.ML	Thu Apr 10 09:08:05 1997 +0200
+++ b/src/ZF/Nat.ML	Thu Apr 10 10:55:37 1997 +0200
@@ -104,7 +104,7 @@
 by (rtac subset_imp_le 1);
 by (rtac subsetI 1);
 by (etac nat_induct 1);
-by (fast_tac (!claset addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
+by (blast_tac (!claset addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
 by (REPEAT (ares_tac [Limit_has_0 RS ltD,
                       Ord_nat, Limit_is_Ord] 1));
 qed "nat_le_Limit";
@@ -186,11 +186,11 @@
 (** nat_case **)
 
 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
-by (fast_tac (!claset addIs [the_equality]) 1);
+by (blast_tac (!claset addIs [the_equality]) 1);
 qed "nat_case_0";
 
 goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
-by (fast_tac (!claset addIs [the_equality]) 1);
+by (blast_tac (!claset addIs [the_equality]) 1);
 qed "nat_case_succ";
 
 Addsimps [nat_case_0, nat_case_succ];