src/ZF/Arith.ML

 
 goal Arith.thy "!!k. [| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
 by (etac rev_mp 1);
 by (etac nat_induct 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 val lemma = result();
 
 (* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
 bind_thm ("zero_lt_natE", lemma RS bexE);
 

     "!!k b. [| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)";
 by (subgoal_tac "k mod 2: 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);
 by (dtac ltD 1);
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "mod2_cases";
 
 goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2: 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);

      "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
 \        !!i. i:k ==> Ord(f(i));                \
 \        i le j;  j:k                           \
 \     |] ==> f(i) le f(j)";
 by (cut_facts_tac prems 1);
-by (fast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
+by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
 qed "Ord_lt_mono_imp_le_mono";
 
 (*le monotonicity, 1st argument*)
 goal Arith.thy
     "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";

 
 (*Thanks to Sten Agerholm*)
 goal Arith.thy  (* add_le_elim1 *)
     "!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
 by (etac rev_mp 1);
-by (eres_inst_tac[("n","n")]nat_induct 1);
+by (eres_inst_tac [("n","n")] nat_induct 1);
 by (Asm_simp_tac 1);
 by (Step_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [not_le_iff_lt,nat_into_Ord]) 1);
 by (etac lt_asym 1);
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [le_iff, nat_into_Ord]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "add_le_elim1";