src/ZF/Univ.ML

--- a/src/ZF/Univ.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Univ.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -40,7 +40,7 @@
 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)";
@@ -71,13 +71,13 @@
 
 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)";
@@ -89,7 +89,7 @@
 
 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 **)
@@ -122,7 +122,7 @@
 
 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))";
@@ -160,7 +160,7 @@
 (*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 ***)
@@ -258,7 +258,7 @@
 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);
@@ -270,7 +270,7 @@
 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";
 
@@ -284,7 +284,7 @@
 
 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
@@ -326,7 +326,7 @@
 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
@@ -345,7 +345,7 @@
 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";
 
@@ -371,7 +371,7 @@
 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
@@ -387,7 +387,7 @@
 
 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;
@@ -402,7 +402,7 @@
 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";
 
@@ -413,7 +413,7 @@
 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)";
@@ -579,7 +579,7 @@
 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));
@@ -614,13 +614,13 @@
 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)";
@@ -628,7 +628,7 @@
 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);