src/ZF/Univ.ML

 
 goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);
 by (stac Vfrom 1);
-by (fast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
 qed "Vfrom_rank_subset1";
 
 goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);

 
 (*** Basic closure properties ***)
 
 goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "zero_in_Vfrom";
 
 goal Univ.thy "i <= Vfrom(A,i)";
 by (eps_ind_tac "i" 1);
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "i_subset_Vfrom";
 
 goal Univ.thy "A <= Vfrom(A,i)";
 by (stac Vfrom 1);
 by (rtac Un_upper1 1);

 
 bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
 
 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_mem_Vfrom";
 
 (** Finite sets and ordered pairs **)
 
 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";

 
 (*** 0, successor and limit equations fof Vfrom ***)
 
 goal Univ.thy "Vfrom(A,0) = A";
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Vfrom_0";
 
 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
 by (rtac (Vfrom RS trans) 1);
 by (rtac (succI1 RS RepFunI RS Union_upper RSN

 by (stac Vfrom 1);
 by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
 (*opposite inclusion*)
 by (rtac UN_least 1);
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Vfrom_Union";
 
 (*** Vfrom applied to Limit ordinals ***)
 
 (*NB. limit ordinals are non-empty;

     "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
 by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
 qed "Inr_in_VLimit";
 
 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (fast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+by (blast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
 qed "sum_VLimit";
 
 bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
 
 

 (*** Properties assuming Transset(A) ***)
 
 goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
 by (eps_ind_tac "i" 1);
 by (stac Vfrom 1);
-by (fast_tac (!claset addSIs [Transset_Union_family, Transset_Un,
+by (blast_tac (!claset addSIs [Transset_Union_family, Transset_Un,
                             Transset_Pow]) 1);
 qed "Transset_Vfrom";
 
 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
 by (rtac (Vfrom_succ RS trans) 1);

 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
 qed "Transset_Vfrom_succ";
 
 goalw Ordinal.thy [Pair_def,Transset_def]
     "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
-by (Best_tac 1);
+by (Blast_tac 1);
 qed "Transset_Pair_subset";
 
 goal Univ.thy
     "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
 \          <a,b> : Vfrom(A,i)";

     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
 \         a*b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
-by (fast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
 qed "prod_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a*b : Vfrom(A,i)";

     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
 \         a+b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
-by (fast_tac (!claset addIs [zero_in_Vfrom, Pair_in_Vfrom, 
+by (blast_tac (!claset addIs [zero_in_Vfrom, Pair_in_Vfrom, 
                            i_subset_Vfrom RS subsetD]) 1);
 qed "sum_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \

 by (rtac (subset_trans RS subset_trans) 1);
 by (rtac Un_upper2 3);
 by (rtac (succI1 RS UN_upper) 2);
 by (rtac Pow_mono 1);
 by (rewtac Transset_def);
-by (fast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
 qed "fun_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a->b : Vfrom(A,i)";

 
 (*** The set Vset(i) ***)
 
 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
 by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Vset";
 
 val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
 
 val Transset_Vset = Transset_0 RS Transset_Vfrom;

 by (rtac (ordi RS trans_induct) 1);
 by (stac Vset 1);
 by (safe_tac (!claset));
 by (stac rank 1);
 by (rtac UN_succ_least_lt 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (REPEAT (ares_tac [ltI] 1));
 qed "Vset_rank_imp1";
 
 (*  [| Ord(i); x : Vset(i) |] ==> rank(x) < i  *)
 bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp));
 
 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
 by (rtac (ordi RS trans_induct) 1);
 by (rtac allI 1);
 by (stac Vset 1);
-by (fast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
 qed "Vset_rank_imp2";
 
 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
 by (etac ltE 1);
 by (etac (Vset_rank_imp2 RS spec RS mp) 1);

 goal Univ.thy "2 : univ(A)";
 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
 qed "two_in_univ";
 
 goalw Univ.thy [bool_def] "bool <= univ(A)";
-by (fast_tac (!claset addSIs [zero_in_univ,one_in_univ]) 1);
+by (blast_tac (!claset addSIs [zero_in_univ,one_in_univ]) 1);
 qed "bool_subset_univ";
 
 bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
 
 

 (** Closure under finite powerset **)
 
 goal Univ.thy
    "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
 by (etac Fin_induct 1);
-by (fast_tac (!claset addSDs [Limit_has_0]) 1);
+by (blast_tac (!claset addSDs [Limit_has_0]) 1);
 by (safe_tac (!claset));
 by (etac Limit_VfromE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x", "xa Un j")] exI 1);
 by (best_tac (!claset addIs [subset_refl RS Vfrom_mono RS subsetD, 
-                           Un_least_lt]) 1);
+			     Un_least_lt]) 1);
 val Fin_Vfrom_lemma = result();
 
 goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
 by (rtac subsetI 1);
 by (dtac Fin_Vfrom_lemma 1);
 by (safe_tac (!claset));
 by (resolve_tac [Vfrom RS ssubst] 1);
-by (fast_tac (!claset addSDs [ltD]) 1);
+by (blast_tac (!claset addSDs [ltD]) 1);
 val Fin_VLimit = result();
 
 bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
 
 goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";