# HG changeset patch
# User paulson
# Date 880020233 -3600
# Node ID d7b8dd96051447551a9d5bd792369d844a9d7f9b
# Parent  97601cf262621c22971e2f02a5b10cd258ba685f
Speeded up the proof of succ_lt_induct_lemma

diff -r 97601cf26262 -r d7b8dd960514 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Thu Nov 20 11:03:26 1997 +0100
+++ b/src/ZF/Nat.ML	Thu Nov 20 11:03:53 1997 +0100
@@ -12,7 +12,7 @@
 by (rtac bnd_monoI 1);
 by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); 
 by (cut_facts_tac [infinity] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "nat_bnd_mono";
 
 (* nat = {0} Un {succ(x). x:nat} *)
@@ -56,7 +56,7 @@
 val major::prems = goal Nat.thy
     "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)";
 by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);
-by (fast_tac (claset() addIs prems) 1);
+by (blast_tac (claset() addIs prems) 1);
 qed "nat_induct";
 
 (*Perform induction on n, then prove the n:nat subgoal using prems. *)
@@ -168,9 +168,9 @@
  "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
 \                 (ALL n:nat. m<n --> P(m,n))";
 by (etac nat_induct 1);
-by (ALLGOALS
+by (ALLGOALS    (*blast_tac gives PROOF FAILED*)
     (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac,
-             fast_tac le_cs, fast_tac le_cs]));
+             best_tac le_cs, best_tac le_cs])); 
 qed "succ_lt_induct_lemma";
 
 val prems = goal Nat.thy