# HG changeset patch
# User paulson
# Date 860582264 -7200
# Node ID b0ae2e13db93cc8f9bff3e73caeea895e45b09e5
# Parent  af506c35b4edb2e5b4a69157b3c4df44e7f54c2b
Using Blast_tac

diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/CardinalArith.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -296,8 +296,9 @@
 
 goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n";
 by (asm_simp_tac 
-    (!simpset addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord,
-                     read_instantiate [("j","0")] cadd_commute, cadd_0]) 1);
+    (!simpset addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, 
+			Card_is_Ord,
+			read_instantiate [("j","0")] cadd_commute, cadd_0]) 1);
 qed "cmult_2";
 
 
@@ -316,8 +317,8 @@
 by (res_inst_tac [("d", "%y. if(y: range(f),    \
 \                               nat_case(u, %z.f`z, converse(f)`y), y)")] 
     lam_injective 1);
-by (fast_tac (!claset addSIs [if_type, nat_0I, nat_succI, apply_type]
-                    addIs  [inj_is_fun, inj_converse_fun]) 1);
+by (fast_tac (!claset addSIs [if_type, nat_succI, apply_type]
+                      addIs  [inj_is_fun, inj_converse_fun]) 1);
 by (asm_simp_tac 
     (!simpset addsimps [inj_is_fun RS apply_rangeI,
                      inj_converse_fun RS apply_rangeI,
@@ -338,7 +339,7 @@
 qed "nat_succ_eqpoll";
 
 goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";
-by (fast_tac (!claset addIs [Card_nat, le_refl, Card_is_Ord]) 1);
+by (blast_tac (!claset addIs [Card_nat, le_refl, Card_is_Ord]) 1);
 qed "InfCard_nat";
 
 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
@@ -412,7 +413,7 @@
 by (rtac (csquareD RS conjE) 1);
 by (rewtac lt_def);
 by (assume_tac 4);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "pred_csquare_subset";
 
 goalw CardinalArith.thy [csquare_rel_def]
@@ -447,11 +448,11 @@
 \         ordermap(K*K, csquare_rel(K)) ` <z,z>";
 by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1);
 by (etac (Limit_is_Ord RS well_ord_csquare) 2);
-by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
+by (blast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
 by (rtac (csquare_ltI RS ordermap_mono RS ltI) 1);
 by (etac well_ord_is_wf 4);
 by (ALLGOALS 
-    (fast_tac (!claset addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] 
+    (blast_tac (!claset addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] 
                      addSEs [ltE])));
 qed "ordermap_z_lt";
 
@@ -462,12 +463,12 @@
 by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1);
 by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1));
 by (subgoals_tac ["z<K"] 1);
-by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
+by (blast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
 by (rtac (ordermap_z_lt RS leI RS le_imp_lepoll RS lepoll_trans) 1);
 by (REPEAT_SOME assume_tac);
 by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1);
 by (etac (Limit_is_Ord RS well_ord_csquare) 1);
-by (fast_tac (!claset addIs [ltD]) 1);
+by (blast_tac (!claset addIs [ltD]) 1);
 by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN
     assume_tac 1);
 by (REPEAT_FIRST (etac ltE));
@@ -601,14 +602,14 @@
 
 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (fast_tac (!claset addSIs [Ord_ordertype]) 2);
+by (blast_tac (!claset addSIs [Ord_ordertype]) 2);
 by (rewtac Transset_def);
 by (safe_tac subset_cs);
 by (asm_full_simp_tac (!simpset addsimps [ordertype_pred_unfold]) 1);
 by (safe_tac (!claset));
 by (rtac UN_I 1);
 by (rtac ReplaceI 2);
-by (ALLGOALS (fast_tac (!claset addSEs [well_ord_subset, predE])));
+by (ALLGOALS (blast_tac (!claset addIs [well_ord_subset] addSEs [predE])));
 qed "Ord_jump_cardinal";
 
 (*Allows selective unfolding.  Less work than deriving intro/elim rules*)
@@ -721,15 +722,15 @@
 by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
 by (assume_tac 1);
 by (resolve_tac [Fin.consI] 1);
-by (Fast_tac 1);
-by (fast_tac (!claset addIs [subset_consI  RS Fin_mono RS subsetD]) 1); 
+by (Blast_tac 1);
+by (blast_tac (!claset addIs [subset_consI  RS Fin_mono RS subsetD]) 1); 
 (*Now for the lemma assumed above*)
 by (rewtac eqpoll_def);
-by (best_tac (!claset addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
 val lemma = result();
 
 goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)";
-by (fast_tac (!claset addIs [lemma RS spec RS mp]) 1);
+by (blast_tac (!claset addIs [lemma RS spec RS mp]) 1);
 qed "Finite_into_Fin";
 
 goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)";
@@ -737,15 +738,15 @@
 qed "Fin_into_Finite";
 
 goal CardinalArith.thy "Finite(A) <-> A : Fin(A)";
-by (fast_tac (!claset addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1);
+by (blast_tac (!claset addIs [Finite_into_Fin, Fin_into_Finite]) 1);
 qed "Finite_Fin_iff";
 
 goal CardinalArith.thy
     "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)";
-by (fast_tac (!claset addSIs [Fin_into_Finite, Fin_UnI] 
-                    addSDs [Finite_into_Fin]
-                    addSEs [Un_upper1 RS Fin_mono RS subsetD,
-                            Un_upper2 RS Fin_mono RS subsetD]) 1);
+by (blast_tac (!claset addSIs [Fin_into_Finite, Fin_UnI] 
+                       addSDs [Finite_into_Fin]
+                       addIs [Un_upper1 RS Fin_mono RS subsetD,
+			      Un_upper2 RS Fin_mono RS subsetD]) 1);
 qed "Finite_Un";
 
 
@@ -757,8 +758,8 @@
 by (simp_tac (!simpset addsimps [lepoll_0_iff]) 1);
 by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1);
 by (Asm_simp_tac 1);
-by (fast_tac (!claset addSDs [cons_lepoll_consD]) 1);
-by (Fast_tac 1);
+by (blast_tac (!claset addSDs [cons_lepoll_consD]) 1);
+by (Blast_tac 1);
 qed "Fin_imp_not_cons_lepoll";
 
 goal CardinalArith.thy
@@ -767,17 +768,17 @@
 by (rtac Least_equality 1);
 by (fold_tac [cardinal_def]);
 by (simp_tac (!simpset addsimps [succ_def]) 1);
-by (fast_tac (!claset addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] 
+by (blast_tac (!claset addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] 
                     addSEs [mem_irrefl]
                     addSDs [Finite_imp_well_ord]) 1);
-by (fast_tac (!claset addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
+by (blast_tac (!claset addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
 by (rtac notI 1);
 by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1);
 by (assume_tac 1);
 by (assume_tac 1);
 by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1);
 by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1);
-by (fast_tac (!claset addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] 
+by (blast_tac (!claset addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] 
                     addSDs [Finite_imp_well_ord]) 1);
 qed "Finite_imp_cardinal_cons";
 
@@ -812,7 +813,7 @@
 qed "nat_sum_eqpoll_sum";
 
 goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
-by (fast_tac (!claset addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
+by (blast_tac (!claset addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
         addSEs [ltE]) 1);
 qed "le_in_nat";
 
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Order.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -18,7 +18,7 @@
 (*needed?*)
 goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def]
     "!!r. part_ord(A,r) ==> asym(r Int A*A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "part_ord_Imp_asym";
 
 val major::premx::premy::prems = goalw Order.thy [linear_def]
@@ -56,14 +56,14 @@
 
 goalw Order.thy [well_ord_def, tot_ord_def]
   "!!r. well_ord(A,r) ==> linear(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "well_ord_is_linear";
 
 
 (** Derived rules for pred(A,x,r) **)
 
 goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_iff";
 
 bind_thm ("predI", conjI RS (pred_iff RS iffD2));
@@ -75,22 +75,22 @@
 qed "predE";
 
 goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_subset_under";
 
 goalw Order.thy [pred_def] "pred(A,x,r) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_subset";
 
 goalw Order.thy [pred_def]
     "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_pred_eq";
 
 goalw Order.thy [trans_on_def, pred_def]
     "!!r. [| trans[A](r);  <y,x>:r;  x:A;  y:A \
 \         |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "trans_pred_pred_eq";
 
 
@@ -100,12 +100,12 @@
 (*Note: a relation s such that s<=r need not be a partial ordering*)
 goalw Order.thy [part_ord_def, irrefl_def, trans_on_def]
     "!!A B r. [| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "part_ord_subset";
 
 goalw Order.thy [linear_def]
     "!!A B r. [| linear(A,r);  B<=A |] ==> linear(B,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "linear_subset";
 
 goalw Order.thy [tot_ord_def]
@@ -122,11 +122,11 @@
 (** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
 
 goalw Order.thy [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "irrefl_Int_iff";
 
 goalw Order.thy [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "trans_on_Int_iff";
 
 goalw Order.thy [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
@@ -134,7 +134,7 @@
 qed "part_ord_Int_iff";
 
 goalw Order.thy [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "linear_Int_iff";
 
 goalw Order.thy [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
@@ -142,7 +142,7 @@
 qed "tot_ord_Int_iff";
 
 goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_Int_iff";
 
 goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
@@ -153,11 +153,11 @@
 (** Relations over the Empty Set **)
 
 goalw Order.thy [irrefl_def] "irrefl(0,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "irrefl_0";
 
 goalw Order.thy [trans_on_def] "trans[0](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "trans_on_0";
 
 goalw Order.thy [part_ord_def] "part_ord(0,r)";
@@ -165,7 +165,7 @@
 qed "part_ord_0";
 
 goalw Order.thy [linear_def] "linear(0,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "linear_0";
 
 goalw Order.thy [tot_ord_def] "tot_ord(0,r)";
@@ -173,7 +173,7 @@
 qed "tot_ord_0";
 
 goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_0";
 
 goalw Order.thy [well_ord_def] "well_ord(0,r)";
@@ -206,12 +206,12 @@
     "[| f: bij(A, B);   \
 \       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
 \    |] ==> f: ord_iso(A,r,B,s)";
-by (fast_tac (!claset addSIs prems) 1);
+by (blast_tac (!claset addSIs prems) 1);
 qed "ord_isoI";
 
 goalw Order.thy [ord_iso_def, mono_map_def]
     "!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
-by (fast_tac (!claset addSDs [bij_is_fun]) 1);
+by (blast_tac (!claset addSDs [bij_is_fun]) 1);
 qed "ord_iso_is_mono_map";
 
 goalw Order.thy [ord_iso_def] 
@@ -223,7 +223,7 @@
 goalw Order.thy [ord_iso_def] 
     "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> \
 \         <f`x, f`y> : s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ord_iso_apply";
 
 goalw Order.thy [ord_iso_def] 
@@ -278,9 +278,9 @@
 \              f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
 by (safe_tac (!claset));
 by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
-by (fast_tac (!claset addIs [apply_type] addSEs [bspec RS bspec RS mp]) 2);
+by (blast_tac (!claset addIs [apply_funtype]) 2);
 by (asm_full_simp_tac (!simpset addsimps [comp_eq_id_iff RS iffD1]) 1);
 qed "mono_ord_isoI";
 
@@ -321,9 +321,8 @@
 by (safe_tac (!claset));
 by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
 by (safe_tac (!claset addSIs [equalityI]));
-by (dtac equalityD1 1);
-by (fast_tac (!claset addSIs [bexI]) 1);
-by (fast_tac (!claset addSIs [bexI] addIs [bij_is_fun RS apply_type]) 1);
+by (ALLGOALS (blast_tac
+	      (!claset addSDs [equalityD1] addIs [bij_is_fun RS apply_type])));
 qed "wf_on_ord_iso";
 
 goalw Order.thy [well_ord_def, tot_ord_def]
@@ -344,7 +343,7 @@
 by (wf_on_ind_tac "y" [] 1);
 by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
 by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "well_ord_iso_subset_lemma";
 
 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
@@ -371,7 +370,7 @@
 by (REPEAT   (*because there are two symmetric cases*)
     (EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS
                           well_ord_iso_predE] 1,
-            fast_tac (!claset addSIs [predI]) 2,
+            blast_tac (!claset addSIs [predI]) 2,
             asm_simp_tac (!simpset addsimps [trans_pred_pred_eq]) 1]));
 qed "well_ord_iso_pred_eq";
 
@@ -385,7 +384,7 @@
 by (rtac equalityI 1);
 by (safe_tac (!claset addSEs [bij_is_fun RS apply_type]));
 by (rtac RepFun_eqI 1);
-by (fast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
+by (blast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
 by (asm_simp_tac bij_inverse_ss 1);
 qed "ord_iso_image_pred";
 
@@ -422,8 +421,8 @@
 by (assume_tac 1);
 qed "well_ord_iso_preserving";
 
-val  bij_apply_cs = !claset addSEs [bij_converse_bij, ord_iso_is_bij]
-                            addIs  [bij_is_fun, apply_type];
+val  bij_apply_cs = !claset addSIs [bij_converse_bij]
+                            addIs  [ord_iso_is_bij, bij_is_fun, apply_funtype];
 
 (*See Halmos, page 72*)
 goal Order.thy
@@ -435,7 +434,7 @@
 by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
 by (safe_tac (!claset));
 by (forward_tac [ord_iso_converse] 1);
-by (REPEAT (fast_tac bij_apply_cs 1));
+by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
 by (asm_full_simp_tac bij_inverse_ss 1);
 qed "well_ord_iso_unique_lemma";
 
@@ -446,7 +445,7 @@
 by (rtac fun_extension 1);
 by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
 by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
-by (REPEAT (fast_tac bij_apply_cs 3));
+by (REPEAT (blast_tac bij_apply_cs 3));
 by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
 by (asm_full_simp_tac (!simpset addsimps [tot_ord_def, well_ord_def]) 2);
 by (linear_case_tac 1);
@@ -456,33 +455,27 @@
 
 (** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
 
-goalw Order.thy [ord_iso_map_def]
-    "ord_iso_map(A,r,B,s) <= A*B";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B";
+by (Blast_tac 1);
 qed "ord_iso_map_subset";
 
-goalw Order.thy [ord_iso_map_def]
-    "domain(ord_iso_map(A,r,B,s)) <= A";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A";
+by (Blast_tac 1);
 qed "domain_ord_iso_map";
 
-goalw Order.thy [ord_iso_map_def]
-    "range(ord_iso_map(A,r,B,s)) <= B";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B";
+by (Blast_tac 1);
 qed "range_ord_iso_map";
 
 goalw Order.thy [ord_iso_map_def]
     "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (fast_tac (!claset addIs [ord_iso_sym]) 1);
+by (blast_tac (!claset addIs [ord_iso_sym]) 1);
 qed "converse_ord_iso_map";
 
 goalw Order.thy [ord_iso_map_def, function_def]
     "!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
-by (safe_tac (!claset));
-by (rtac well_ord_iso_pred_eq 1);
-by (REPEAT_SOME assume_tac);
-by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
-by (assume_tac 1);
+by (blast_tac (!claset addIs [well_ord_iso_pred_eq, 
+			      ord_iso_sym, ord_iso_trans]) 1);
 qed "function_ord_iso_map";
 
 goal Order.thy
@@ -501,8 +494,9 @@
 by (safe_tac (!claset));
 by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
 by (REPEAT 
-    (fast_tac (!claset addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
-by (asm_simp_tac (!simpset addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
+    (blast_tac (!claset addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
+by (asm_simp_tac 
+    (!simpset addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
 by (rewtac ord_iso_map_def);
 by (safe_tac (!claset addSEs [UN_E]));
 by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
@@ -531,7 +525,7 @@
 by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
 by (linear_case_tac 1);
 (*Trivial case: a=xa*)
-by (Fast_tac 2);
+by (Blast_tac 2);
 (*Harder case: <a, xa>: r*)
 by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
     REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
@@ -539,7 +533,7 @@
     REPEAT1 (eresolve_tac [asm_rl, predI] 1));
 by (asm_full_simp_tac
     (!simpset addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "domain_ord_iso_map_subset";
 
 (*For the 4-way case analysis in the main result*)
@@ -559,7 +553,7 @@
 by (assume_tac 2);
 by (rtac equalityI 1);
 (*not (!claset) below; that would use rules like domainE!*)
-by (fast_tac (!claset addSEs [predE]) 2);
+by (blast_tac (!claset addSEs [predE]) 2);
 by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
 qed "domain_ord_iso_map_cases";
 
@@ -591,7 +585,7 @@
 by (dtac rangeI 1);
 by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
 by (rewtac ord_iso_map_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "well_ord_trichotomy";
 
 
@@ -599,27 +593,27 @@
 
 goalw Order.thy [irrefl_def] 
             "!!A. irrefl(A,r) ==> irrefl(A,converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
 qed "irrefl_converse";
 
 goalw Order.thy [trans_on_def] 
     "!!A. trans[A](r) ==> trans[A](converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
 qed "trans_on_converse";
 
 goalw Order.thy [part_ord_def] 
     "!!A. part_ord(A,r) ==> part_ord(A,converse(r))";
-by (fast_tac (!claset addSIs [irrefl_converse, trans_on_converse]) 1);
+by (blast_tac (!claset addSIs [irrefl_converse, trans_on_converse]) 1);
 qed "part_ord_converse";
 
 goalw Order.thy [linear_def] 
     "!!A. linear(A,r) ==> linear(A,converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
 qed "linear_converse";
 
 goalw Order.thy [tot_ord_def] 
     "!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))";
-by (fast_tac (!claset addSIs [part_ord_converse, linear_converse]) 1);
+by (blast_tac (!claset addSIs [part_ord_converse, linear_converse]) 1);
 qed "tot_ord_converse";
 
 
@@ -627,7 +621,7 @@
     Lemmas involving the first element of a well ordered set **)
 
 goalw thy [first_def] "!!b. first(b,B,r) ==> b:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "first_is_elem";
 
 goalw thy [well_ord_def, wf_on_def, wf_def,     first_def] 
@@ -636,9 +630,9 @@
 by (contr_tac 1);
 by (etac bexE 1);
 by (res_inst_tac [("a","x")] ex1I 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (rewrite_goals_tac [tot_ord_def, linear_def]);
-by (Fast_tac 1);
+by (Blast.depth_tac (!claset) 7 1);
 qed "well_ord_imp_ex1_first";
 
 goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/OrderArith.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -15,22 +15,22 @@
 
 goalw OrderArith.thy [radd_def] 
     "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "radd_Inl_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "radd_Inl_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "radd_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "radd_Inr_Inl_iff";
 
 (** Elimination Rule **)
@@ -43,7 +43,7 @@
 \    |] ==> Q";
 by (cut_facts_tac [major] 1);
 (*Split into the three cases*)
-by (REPEAT_FIRST
+by (REPEAT_FIRST  (*can't use safe_tac: don't want hyp_subst_tac*)
     (eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
 (*Apply each premise to correct subgoal; can't just use fast_tac
   because hyp_subst_tac would delete equalities too quickly*)
@@ -83,14 +83,14 @@
 by (rtac ballI 2);
 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
 by (etac (bspec RS mp) 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (best_tac (!claset addSEs [raddE]) 2);
 (*Returning to main part of proof*)
 by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
 by (Best_tac 1);
 by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
 by (etac (bspec RS mp) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (best_tac (!claset addSEs [raddE]) 1);
 qed "wf_on_radd";
 
@@ -143,11 +143,11 @@
 \           (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
 by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] 
     lam_bijective 1);
-by (fast_tac (!claset addSIs [if_type]) 2);
+by (blast_tac (!claset addSIs [if_type]) 2);
 by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
 by (safe_tac (!claset));
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 qed "sum_disjoint_bij";
 
 (** Associativity **)
@@ -178,7 +178,7 @@
     "!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <->       \
 \           (<a',a>: r  & a':A & a:A & b': B & b: B) |  \
 \           (<b',b>: s  & a'=a & a:A & b': B & b: B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rmult_iff";
 
 Addsimps [rmult_iff];
@@ -209,7 +209,7 @@
 by (Asm_simp_tac 1);
 by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
 by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
-by (REPEAT_SOME (Fast_tac));
+by (REPEAT_SOME (Blast_tac));
 qed "linear_rmult";
 
 
@@ -221,12 +221,12 @@
 by (etac SigmaE 1);
 by (etac ssubst 1);
 by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
 by (rtac ballI 1);
 by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
 by (etac (bspec RS mp) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (best_tac (!claset addSEs [rmultE]) 1);
 qed "wf_on_rmult";
 
@@ -266,7 +266,7 @@
 by (safe_tac (!claset addSIs [prod_bij]));
 by (ALLGOALS
     (asm_full_simp_tac (!simpset addsimps [bij_is_fun RS apply_type])));
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (fast_tac (!claset addSEs [bij_is_inj RS inj_apply_equality]) 1);
 qed "prod_ord_iso_cong";
 
@@ -282,7 +282,7 @@
 \         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
 by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
 by (Asm_simp_tac 1);
-by (fast_tac (!claset addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
+by (blast_tac (!claset addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
 qed "singleton_prod_ord_iso";
 
 (*Here we build a complicated function term, then simplify it using
@@ -295,7 +295,7 @@
 by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
 by (rtac singleton_prod_bij 1);
 by (rtac sum_disjoint_bij 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (asm_simp_tac (!simpset addcongs [case_cong] addsimps [id_conv]) 1);
 by (resolve_tac [comp_lam RS trans RS sym] 1);
 by (fast_tac (!claset addSEs [case_type]) 1);
@@ -352,7 +352,7 @@
 by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
 by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst]));
 by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "prod_assoc_ord_iso";
 
 (**** Inverse image of a relation ****)
@@ -361,7 +361,7 @@
 
 goalw OrderArith.thy [rvimage_def] 
     "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rvimage_iff";
 
 (** Type checking **)
@@ -374,7 +374,7 @@
 
 goalw OrderArith.thy [rvimage_def] 
     "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rvimage_converse";
 
 
@@ -382,17 +382,17 @@
 
 goalw OrderArith.thy [irrefl_def, rvimage_def]
     "!!A B. [| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
-by (fast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
 qed "irrefl_rvimage";
 
 goalw OrderArith.thy [trans_on_def, rvimage_def] 
     "!!A B. [| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
-by (fast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
 qed "trans_on_rvimage";
 
 goalw OrderArith.thy [part_ord_def]
     "!!A B. [| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
-by (fast_tac (!claset addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
+by (blast_tac (!claset addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
 qed "part_ord_rvimage";
 
 (** Linearity **)
@@ -404,12 +404,12 @@
 by (asm_simp_tac (!simpset addsimps [rvimage_iff]) 1);
 by (cut_facts_tac [finj] 1);
 by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
-by (REPEAT_SOME (fast_tac (!claset addSIs [apply_type])));
+by (REPEAT_SOME (blast_tac (!claset addIs [apply_funtype])));
 qed "linear_rvimage";
 
 goalw OrderArith.thy [tot_ord_def] 
     "!!A B. [| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
-by (fast_tac (!claset addSIs [part_ord_rvimage, linear_rvimage]) 1);
+by (blast_tac (!claset addSIs [part_ord_rvimage, linear_rvimage]) 1);
 qed "tot_ord_rvimage";
 
 
@@ -419,10 +419,11 @@
     "!!r. [| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
 by (rtac wf_onI2 1);
 by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
-by (fast_tac (!claset addSIs [apply_type]) 1);
-by (best_tac (!claset addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
+by (blast_tac (!claset addSIs [apply_funtype]) 1);
+by (blast_tac (!claset addSIs [apply_funtype] 
+                       addSDs [rvimage_iff RS iffD1]) 1);
 qed "wf_on_rvimage";
 
 (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
@@ -430,8 +431,8 @@
     "!!r. [| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
 by (rtac well_ordI 1);
 by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
-by (fast_tac (!claset addSIs [wf_on_rvimage, inj_is_fun]) 1);
-by (fast_tac (!claset addSIs [linear_rvimage]) 1);
+by (blast_tac (!claset addSIs [wf_on_rvimage, inj_is_fun]) 1);
+by (blast_tac (!claset addSIs [linear_rvimage]) 1);
 qed "well_ord_rvimage";
 
 goalw OrderArith.thy [ord_iso_def]
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/OrderType.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -32,12 +32,12 @@
 goalw OrderType.thy [pred_def, lt_def]
     "!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
 by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (!claset addEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
 qed "lt_pred_Memrel";
 
 goalw OrderType.thy [pred_def,Memrel_def] 
       "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_Memrel";
 
 goal OrderType.thy
@@ -108,7 +108,7 @@
 by (asm_simp_tac (!simpset addsimps [ordermap_pred_unfold]) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
 by (rewrite_goals_tac [pred_def,Transset_def]);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (safe_tac (!claset));
 by (ordermap_elim_tac 1);
 by (fast_tac (!claset addSEs [trans_onD]) 1);
@@ -118,11 +118,11 @@
     "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
 by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (fast_tac (!claset addIs [Ord_ordermap]) 2);
+by (blast_tac (!claset addIs [Ord_ordermap]) 2);
 by (rewrite_goals_tac [Transset_def,well_ord_def]);
 by (safe_tac (!claset));
 by (ordermap_elim_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Ord_ordertype";
 
 (*** ordermap preserves the orderings in both directions ***)
@@ -132,7 +132,7 @@
 \         ordermap(A,r)`w : ordermap(A,r)`x";
 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
 by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ordermap_mono";
 
 (*linearity of r is crucial here*)
@@ -141,7 +141,7 @@
 \            w: A; x: A |] ==> <w,x>: r";
 by (safe_tac (!claset));
 by (linear_case_tac 1);
-by (fast_tac (!claset addSEs [mem_not_refl RS notE]) 1);
+by (blast_tac (!claset addSEs [mem_not_refl RS notE]) 1);
 by (dtac ordermap_mono 1);
 by (REPEAT_SOME assume_tac);
 by (etac mem_asym 1);
@@ -165,13 +165,10 @@
 goalw OrderType.thy [ord_iso_def]
  "!!r. well_ord(A,r) ==> \
 \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
-by (safe_tac (!claset));
-by (rtac ordermap_bij 1);
-by (assume_tac 1);
-by (fast_tac (!claset addSEs [MemrelE, converse_ordermap_mono]) 2);
-by (rewtac well_ord_def);
-by (fast_tac (!claset addSIs [MemrelI, ordermap_mono,
-                            ordermap_type RS apply_type]) 1);
+by (safe_tac (!claset addSEs [well_ord_is_wf]
+		      addSIs [ordermap_type RS apply_type,
+			      ordermap_mono, ordermap_bij]));
+by (blast_tac (!claset addSDs [converse_ordermap_mono]) 1);
 qed "ordertype_ord_iso";
 
 goal OrderType.thy
@@ -252,12 +249,12 @@
 (** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
 
 goal OrderType.thy
-    "!!r. [| well_ord(A,r);  x:A |] ==>  \
+    "!!r. [| well_ord(A,r);  x:A |] ==>             \
 \         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
 by (asm_simp_tac (!simpset addsimps [ordertype_unfold, 
                   pred_subset RSN (2, well_ord_subset)]) 1);
-by (fast_tac (!claset addIs [ordermap_pred_eq_ordermap, RepFun_eqI]
-                    addEs [predE]) 1);
+by (fast_tac (!claset addIs [ordermap_pred_eq_ordermap]
+                      addEs [predE]) 1);
 qed "ordertype_pred_subset";
 
 goal OrderType.thy
@@ -295,7 +292,7 @@
 by (rtac conjI 1);
 by (etac well_ord_Memrel 1);
 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (Fast_tac 1);
+by (Blast.depth_tac (!claset) 8 1);
 qed "Ord_is_Ord_alt";
 
 (*proof by lcp*)
@@ -303,12 +300,7 @@
                      tot_ord_def, part_ord_def, trans_on_def] 
     "!!i. Ord_alt(i) ==> Ord(i)";
 by (asm_full_simp_tac (!simpset addsimps [Memrel_iff, pred_Memrel]) 1);
-by (safe_tac (!claset));
-by (fast_tac (!claset addSDs [equalityD1]) 1);
-by (subgoal_tac "xa: i" 1);
-by (fast_tac (!claset addSDs [equalityD1]) 2);
-by (fast_tac (!claset addSDs [equalityD1]
-                    addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Ord_alt_is_Ord";
 
 
@@ -321,7 +313,7 @@
 goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
 by (res_inst_tac [("d", "Inl")] lam_bijective 1);
 by (safe_tac (!claset));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "bij_sum_0";
 
 goal OrderType.thy
@@ -334,7 +326,7 @@
 goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
 by (res_inst_tac [("d", "Inr")] lam_bijective 1);
 by (safe_tac (!claset));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "bij_0_sum";
 
 goal OrderType.thy
@@ -433,7 +425,7 @@
     "!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
 by (resolve_tac [id_bij RS ord_isoI] 1);
 by (asm_simp_tac (!simpset addsimps [id_conv, Memrel_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "id_ord_iso_Memrel";
 
 goal OrderType.thy
@@ -517,13 +509,13 @@
 by (REPEAT (ares_tac [Ord_oadd] 1));
 by (fast_tac (!claset addIs [lt_oadd1, oadd_lt_mono2]
                     addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
-by (Fast_tac 2);
-by (fast_tac (!claset addSEs [ltE]) 1);
+by (Blast_tac 2);
+by (blast_tac (!claset addSEs [ltE]) 1);
 qed "oadd_unfold";
 
 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
 by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "oadd_1";
 
 goal OrderType.thy
@@ -539,7 +531,7 @@
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (fast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
+by (blast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
                                     lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
 qed "oadd_UN";
@@ -561,7 +553,7 @@
 by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
                                      le_refl, Limit_is_Ord]) 1);
 qed "oadd_le_self2";
@@ -574,7 +566,7 @@
 by (asm_simp_tac (!simpset addsimps [oadd_succ, succ_le_iff]) 1);
 by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
 by (rtac le_implies_UN_le_UN 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "oadd_le_mono1";
 
 goal OrderType.thy "!!i j. [| i' le i;  j'<j |] ==> i'++j' < i++j";
@@ -601,7 +593,7 @@
 goal OrderType.thy
     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (fast_tac (!claset addSIs [if_type]) 1);
+by (blast_tac (!claset addSIs [if_type]) 1);
 by (fast_tac (!claset addSIs [case_type]) 1);
 by (etac sumE 2);
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
@@ -620,7 +612,7 @@
 by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
 by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
-by (fast_tac (!claset addEs [lt_trans2, lt_trans]) 1);
+by (blast_tac (!claset addIs [lt_trans2, lt_trans]) 1);
 qed "ordertype_sum_Diff";
 
 goalw OrderType.thy [oadd_def, odiff_def]
@@ -681,7 +673,7 @@
 by (rtac equalityI 1);
 by (safe_tac (!claset));
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
 qed "pred_Pair_eq";
 
 goal OrderType.thy
@@ -693,7 +685,7 @@
 by (resolve_tac [ordertype_eq RS sym] 1);
 by (rtac prod_sum_singleton_ord_iso 1);
 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
-by (fast_tac (!claset addSEs [predE]) 1);
+by (blast_tac (!claset addSEs [predE]) 1);
 qed "ordertype_pred_Pair_eq";
 
 goalw OrderType.thy [oadd_def, omult_def]
@@ -724,7 +716,7 @@
 by (step_tac (!claset addSEs [ltE]) 1);
 by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
                                   symmetric omult_def]) 1);
-by (fast_tac (!claset addIs [ltI]) 1);
+by (blast_tac (!claset addIs [ltI]) 1);
 qed "lt_omult";
 
 goalw OrderType.thy [omult_def]
@@ -737,7 +729,7 @@
     (!simpset addsimps [ordertype_pred_unfold, 
                      well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
 by (rtac bexI 1);
-by (fast_tac (!claset addSEs [ltE]) 2);
+by (blast_tac (!claset addSEs [ltE]) 2);
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
                         symmetric omult_def]) 1);
@@ -749,8 +741,8 @@
 by (resolve_tac [lt_omult RS exE] 1);
 by (etac ltI 3);
 by (REPEAT (ares_tac [Ord_omult] 1));
-by (fast_tac (!claset addSEs [ltE]) 1);
-by (fast_tac (!claset addIs [omult_oadd_lt RS ltD, ltI]) 1);
+by (blast_tac (!claset addSEs [ltE]) 1);
+by (blast_tac (!claset addIs [omult_oadd_lt RS ltD, ltI]) 1);
 qed "omult_unfold";
 
 (*** Basic laws for ordinal multiplication ***)
@@ -832,7 +824,7 @@
     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
 \    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
 by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "omult_UN";
 
 goal OrderType.thy 
@@ -866,7 +858,7 @@
 by (asm_simp_tac (!simpset addsimps [omult_succ, oadd_le_mono]) 1);
 by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
 by (rtac le_implies_UN_le_UN 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "omult_le_mono1";
 
 goal OrderType.thy "!!i j k. [| k<j;  0<i |] ==> i**k < i**j";
@@ -909,7 +901,7 @@
 by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
                                      Limit_is_Ord RS le_refl]) 1);
 qed "omult_le_self2";
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Ordinal.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -13,75 +13,75 @@
 (** Two neat characterisations of Transset **)
 
 goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_iff_Pow";
 
 goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Transset_iff_Union_succ";
 
 (** Consequences of downwards closure **)
 
 goalw Ordinal.thy [Transset_def]
     "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_doubleton_D";
 
 val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
     "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
 by (cut_facts_tac [prem2] 1);   
-by (fast_tac (!claset addSDs [prem1 RS Transset_doubleton_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_doubleton_D]) 1);
 qed "Transset_Pair_D";
 
 val prem1::prems = goal Ordinal.thy
     "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
 qed "Transset_includes_domain";
 
 val prem1::prems = goal Ordinal.thy
     "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
 qed "Transset_includes_range";
 
 (** Closure properties **)
 
 goalw Ordinal.thy [Transset_def] "Transset(0)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_0";
 
 goalw Ordinal.thy [Transset_def]
     "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_Un";
 
 goalw Ordinal.thy [Transset_def]
     "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_Int";
 
 goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_succ";
 
 goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_Pow";
 
 goalw Ordinal.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Transset_Union";
 
 val [Transprem] = goalw Ordinal.thy [Transset_def]
     "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
-by (fast_tac (!claset addEs [Transprem RS bspec RS subsetD]) 1);
+by (blast_tac (!claset addDs [Transprem RS bspec RS subsetD]) 1);
 qed "Transset_Union_family";
 
 val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
     "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
 by (cut_facts_tac [prem] 1);
-by (fast_tac (!claset addEs [Transprem RS bspec RS subsetD]) 1);
+by (blast_tac (!claset addDs [Transprem RS bspec RS subsetD]) 1);
 qed "Transset_Inter_family";
 
 (*** Natural Deduction rules for Ord ***)
@@ -104,7 +104,7 @@
 (*** Lemmas for ordinals ***)
 
 goalw Ordinal.thy [Ord_def,Transset_def] "!!i j.[| Ord(i);  j:i |] ==> Ord(j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Ord_in_Ord";
 
 (* Ord(succ(j)) ==> Ord(j) *)
@@ -116,7 +116,7 @@
 qed "Ord_subset_Ord";
 
 goalw Ordinal.thy [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "OrdmemD";
 
 goal Ordinal.thy "!!i j k. [| i:j;  j:k;  Ord(k) |] ==> i:k";
@@ -143,18 +143,18 @@
 bind_thm ("Ord_1", Ord_0 RS Ord_succ);
 
 goal Ordinal.thy "Ord(succ(i)) <-> Ord(i)";
-by (fast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (blast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
 qed "Ord_succ_iff";
 
 Addsimps [Ord_0, Ord_succ_iff];
 AddSIs   [Ord_0, Ord_succ];
 
 goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
-by (fast_tac (!claset addSIs [Transset_Un]) 1);
+by (blast_tac (!claset addSIs [Transset_Un]) 1);
 qed "Ord_Un";
 
 goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
-by (fast_tac (!claset addSIs [Transset_Int]) 1);
+by (blast_tac (!claset addSIs [Transset_Int]) 1);
 qed "Ord_Int";
 
 val nonempty::prems = goal Ordinal.thy
@@ -179,7 +179,7 @@
 by (forw_inst_tac [("x", "X")] spec 1);
 by (safe_tac (!claset addSEs [mem_irrefl]));
 by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (rewtac Transset_def);
 by (safe_tac (!claset));
 by (Asm_full_simp_tac 1);
@@ -204,7 +204,7 @@
 qed "ltD";
 
 goalw Ordinal.thy [lt_def] "~ i<0";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "not_lt0";
 
 Addsimps [not_lt0];
@@ -224,7 +224,7 @@
 bind_thm ("lt0E", not_lt0 RS notE);
 
 goal Ordinal.thy "!!i j k. [| i<j;  j<k |] ==> i<k";
-by (fast_tac (!claset addSIs [ltI] addSEs [ltE, Ord_trans]) 1);
+by (blast_tac (!claset addSIs [ltI] addSEs [ltE] addIs [Ord_trans]) 1);
 qed "lt_trans";
 
 goalw Ordinal.thy [lt_def] "!!i j. [| i<j;  j<i |] ==> P";
@@ -242,7 +242,7 @@
 (** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
 
 goalw Ordinal.thy [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
-by (fast_tac (!claset addSIs [Ord_succ] addSDs [Ord_succD]) 1);
+by (blast_tac (!claset addSIs [Ord_succ] addSDs [Ord_succD]) 1);
 qed "le_iff";
 
 (*Equivalently, i<j ==> i < succ(j)*)
@@ -269,11 +269,11 @@
 
 goal Ordinal.thy "!!i j. [| i le j;  j le i |] ==> i=j";
 by (asm_full_simp_tac (!simpset addsimps [le_iff]) 1);
-by (fast_tac (!claset addEs [lt_asym]) 1);
+by (blast_tac (!claset addEs [lt_asym]) 1);
 qed "le_anti_sym";
 
 goal Ordinal.thy "i le 0 <-> i=0";
-by (fast_tac (!claset addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
+by (blast_tac (!claset addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
 qed "le0_iff";
 
 bind_thm ("le0D", le0_iff RS iffD1);
@@ -282,17 +282,18 @@
 AddSDs [le0D];
 Addsimps [le0_iff];
 
+(*blast_tac will NOT see lt_asym*)
 val le_cs = !claset addSIs [leCI] addSEs [leE] addEs [lt_asym];
 
 
 (*** Natural Deduction rules for Memrel ***)
 
 goalw Ordinal.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Memrel_iff";
 
-val prems = goal Ordinal.thy "[| a: b;  a: A;  b: A |] ==> <a,b> : Memrel(A)";
-by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
+goal Ordinal.thy "!!A. [| a: b;  a: A;  b: A |] ==> <a,b> : Memrel(A)";
+by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
 qed "MemrelI";
 
 val [major,minor] = goal Ordinal.thy
@@ -305,20 +306,23 @@
 by (REPEAT (assume_tac 1));
 qed "MemrelE";
 
+AddSIs [MemrelI];
+AddSEs [MemrelE];
+
 goalw Ordinal.thy [Memrel_def] "Memrel(A) <= A*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Memrel_type";
 
 goalw Ordinal.thy [Memrel_def] "!!A B. A<=B ==> Memrel(A) <= Memrel(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Memrel_mono";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(0) = 0";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Memrel_0";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(1) = 0";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Memrel_1";
 
 Addsimps [Memrel_0, Memrel_1];
@@ -338,13 +342,13 @@
 (*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
 goalw Ordinal.thy [Ord_def, Transset_def, trans_def]
     "!!i. Ord(i) ==> trans(Memrel(i))";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (Blast_tac 1);
 qed "trans_Memrel";
 
 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
 goalw Ordinal.thy [Transset_def]
     "!!A. Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (Blast_tac 1);
 qed "Transset_Memrel_iff";
 
 
@@ -356,11 +360,11 @@
 \       !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) \
 \    |]  ==>  P(i)";
 by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
-by (fast_tac (!claset addEs [MemrelE]) 1);
+by (Blast_tac 1);
 by (resolve_tac prems 1);
 by (assume_tac 1);
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [MemrelI]) 1);
+by (Blast_tac 1);
 qed "Transset_induct";
 
 (*Induction over an ordinal*)
@@ -423,19 +427,19 @@
 qed "Ord_linear_le";
 
 goal Ordinal.thy "!!i j. j le i ==> ~ i<j";
-by (fast_tac le_cs 1);
+by (blast_tac le_cs 1);
 qed "le_imp_not_lt";
 
 goal Ordinal.thy "!!i j. [| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1);
 by (REPEAT (SOMEGOAL assume_tac));
-by (fast_tac le_cs 1);
+by (blast_tac le_cs 1);
 qed "not_lt_imp_le";
 
 (** Some rewrite rules for <, le **)
 
 goalw Ordinal.thy [lt_def] "!!i j. Ord(j) ==> i:j <-> i<j";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Ord_mem_iff_lt";
 
 goal Ordinal.thy "!!i j. [| Ord(i);  Ord(j) |] ==> ~ i<j <-> j le i";
@@ -455,7 +459,7 @@
 goal Ordinal.thy "!!i. [| Ord(i);  i~=0 |] ==> 0<i";
 by (etac (not_le_iff_lt RS iffD1) 1);
 by (rtac Ord_0 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Ord_0_lt";
 
 (*** Results about less-than or equals ***)
@@ -466,23 +470,23 @@
 by (rtac (not_lt_iff_le RS iffD1) 1);
 by (assume_tac 1);
 by (assume_tac 1);
-by (fast_tac (!claset addEs [ltE, mem_irrefl]) 1);
+by (blast_tac (!claset addEs [ltE, mem_irrefl]) 1);
 qed "subset_imp_le";
 
 goal Ordinal.thy "!!i j. i le j ==> i<=j";
 by (etac leE 1);
-by (Fast_tac 2);
-by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
+by (Blast_tac 2);
+by (blast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
 qed "le_imp_subset";
 
 goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)";
 by (fast_tac (!claset addSEs [subset_imp_le, le_imp_subset]
-                    addEs [ltE, make_elim Ord_succD]) 1);
+                      addEs [ltE, make_elim Ord_succD]) 1);
 qed "le_subset_iff";
 
 goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
 by (simp_tac (!simpset addsimps [le_iff]) 1);
-by (fast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (blast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
 qed "le_succ_iff";
 
 (*Just a variant of subset_imp_le*)
@@ -495,11 +499,11 @@
 (** Transitive laws **)
 
 goal Ordinal.thy "!!i j. [| i le j;  j<k |] ==> i<k";
-by (fast_tac (!claset addEs [leE, lt_trans]) 1);
+by (blast_tac (!claset addSEs [leE] addIs [lt_trans]) 1);
 qed "lt_trans1";
 
 goal Ordinal.thy "!!i j. [| i<j;  j le k |] ==> i<k";
-by (fast_tac (!claset addEs [leE, lt_trans]) 1);
+by (blast_tac (!claset addSEs [leE] addIs [lt_trans]) 1);
 qed "lt_trans2";
 
 goal Ordinal.thy "!!i j. [| i le j;  j le k |] ==> i le k";
@@ -508,15 +512,15 @@
 
 goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
 by (rtac (not_lt_iff_le RS iffD1) 1);
-by (fast_tac le_cs 3);
-by (ALLGOALS (fast_tac (!claset addEs [ltE] addIs [Ord_succ])));
+by (blast_tac le_cs 3);
+by (ALLGOALS (blast_tac (!claset addEs [ltE] addIs [Ord_succ])));
 qed "succ_leI";
 
 (*Identical to  succ(i) < succ(j) ==> i<j  *)
 goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
 by (rtac (not_le_iff_lt RS iffD1) 1);
 by (fast_tac le_cs 3);
-by (ALLGOALS (fast_tac (!claset addEs [ltE, make_elim Ord_succD])));
+by (ALLGOALS (blast_tac (!claset addEs [ltE, make_elim Ord_succD])));
 qed "succ_leE";
 
 goal Ordinal.thy "succ(i) le j <-> i<j";
@@ -526,7 +530,7 @@
 Addsimps [succ_le_iff];
 
 goal Ordinal.thy "!!i j. succ(i) le succ(j) ==> i le j";
-by (fast_tac (!claset addSEs [succ_leE]) 1);
+by (blast_tac (!claset addSDs [succ_leE]) 1);
 qed "succ_le_imp_le";
 
 (** Union and Intersection **)
@@ -647,14 +651,14 @@
 qed "Limit_has_0";
 
 goalw Ordinal.thy [Limit_def] "!!i. [| Limit(i);  j<i |] ==> succ(j) < i";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Limit_has_succ";
 
 goalw Ordinal.thy [Limit_def]
     "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
 by (safe_tac subset_cs);
 by (rtac (not_le_iff_lt RS iffD1) 2);
-by (fast_tac le_cs 4);
+by (blast_tac le_cs 4);
 by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
 qed "non_succ_LimitI";
 
@@ -672,7 +676,7 @@
 (** Traditional 3-way case analysis on ordinals **)
 
 goal Ordinal.thy "!!i. Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
-by (fast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
+by (blast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
                       addSDs [Ord_succD]) 1);
 qed "Ord_cases_disj";
 
@@ -694,5 +698,5 @@
 \     |] ==> P(i)";
 by (resolve_tac [major RS trans_induct] 1);
 by (etac Ord_cases 1);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
 qed "trans_induct3";
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Sum.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -17,7 +17,7 @@
 
 goalw Sum.thy [Part_def]
     "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_eqI";
 
 val PartI = refl RSN (2,Part_eqI);
@@ -30,7 +30,7 @@
 by (REPEAT (ares_tac prems 1));
 qed "PartE";
 
-AddSIs [PartI];
+AddIs  [Part_eqI];
 AddSEs [PartE];
 
 goalw Sum.thy [Part_def] "Part(A,h) <= A";
@@ -43,17 +43,17 @@
 val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
 
 goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Sigma_bool";
 
 (** Introduction rules for the injections **)
 
 goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InlI";
 
 goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InrI";
 
 (** Elimination rules **)
@@ -104,28 +104,28 @@
 Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
 
 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InlD";
 
 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InrD";
 
 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sum_iff";
 
 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sum_subset_iff";
 
 goal Sum.thy "A+B = C+D <-> A=C & B=D";
 by (simp_tac (!simpset addsimps [extension,sum_subset_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sum_equal_iff";
 
 goalw Sum.thy [sum_def] "A+A = 2*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sum_eq_2_times";
 
 
@@ -179,21 +179,21 @@
 (*** More rules for Part(A,h) ***)
 
 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_mono";
 
 goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_Collect";
 
 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
 
 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_Inl";
 
 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_Inr";
 
 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -201,13 +201,13 @@
 qed "PartD1";
 
 goal Sum.thy "Part(A,%x.x) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_id";
 
 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_Inr2";
 
 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_sum_equality";
diff -r af506c35b4ed -r b0ae2e13db93 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);
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/ZF.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -438,7 +438,6 @@
  (fn _=> [ Blast_tac 1 ]);
 
 Addsimps [empty_subsetI];
-AddSIs [empty_subsetI];
 
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
  (fn prems=> [ blast_tac (!claset addDs prems) 1 ]);
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Zorn.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -14,12 +14,12 @@
 (*** Section 1.  Mathematical Preamble ***)
 
 goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_lemma0";
 
 goal ZF.thy
     "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_lemma0";
 
 
@@ -73,7 +73,7 @@
 \    |] ==> n<=m | next`m<=n";
 by (cut_facts_tac prems 1);
 by (rtac (major RS TFin_induct) 1);
-by (etac Union_lemma0 2);               (*or just Fast_tac*)
+by (etac Union_lemma0 2);               (*or just Blast_tac*)
 by (fast_tac (subset_cs addIs [increasing_trans]) 1);
 qed "TFin_linear_lemma1";
 
@@ -173,7 +173,7 @@
 \         |] ==> ch ` super(S,X) : super(S,X)";
 by (etac apply_type 1);
 by (rewrite_goals_tac [super_def, maxchain_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "choice_super";
 
 goal Zorn.thy
@@ -210,7 +210,7 @@
 by (dtac choice_super 1);
 by (REPEAT (assume_tac 1));
 by (rewtac super_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Hausdorff_next_exists";
 
 (*Lemma 4*)
@@ -227,13 +227,10 @@
                      choice_super RS (super_subset_chain RS subsetD)]
            setloop split_tac [expand_if]) 1);
 by (rewtac chain_def);
-by (rtac CollectI 1 THEN Fast_tac 1);
-(*Cannot use safe_tac: the disjunction must be left alone*)
-by (REPEAT (rtac ballI 1 ORELSE etac UnionE 1));
+by (rtac CollectI 1 THEN Blast_tac 1);
+by (safe_tac(!claset));
 by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
-(*fast_tac is just too slow here!*)
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, subsetD] 1
-       ORELSE ball_tac 1 THEN etac (CollectD2 RS bspec RS bspec) 1));
+by (ALLGOALS Fast_tac);
 qed "TFin_chain_lemma4";
 
 goal Zorn.thy "EX c. c : maxchain(S)";
@@ -265,7 +262,7 @@
 (*Used in the proof of Zorn's Lemma*)
 goalw Zorn.thy [chain_def]
     "!!c. [| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "chain_extend";
 
 goal Zorn.thy
@@ -274,16 +271,16 @@
 by (asm_full_simp_tac (!simpset addsimps [maxchain_def]) 1);
 by (rename_tac "c" 1);
 by (res_inst_tac [("x", "Union(c)")] bexI 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (safe_tac (!claset));
 by (rename_tac "z" 1);
 by (rtac classical 1);
 by (subgoal_tac "cons(z,c): super(S,c)" 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 by (rewtac super_def);
 by (safe_tac (!claset));
 by (fast_tac (!claset addEs [chain_extend]) 1);
-by (best_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 qed "Zorn";
 
 
@@ -295,13 +292,13 @@
 \    |] ==> ALL m:Z. n<=m";
 by (cut_facts_tac prems 1);
 by (rtac (major RS TFin_induct) 1);
-by (Fast_tac 2);                  (*second induction step is easy*)
+by (Blast_tac 2);                  (*second induction step is easy*)
 by (rtac ballI 1);
 by (rtac (bspec RS TFin_subsetD RS disjE) 1);
 by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
 by (subgoal_tac "x = Inter(Z)" 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed "TFin_well_lemma5";
 
 (*Well-ordering of TFin(S,next)*)
@@ -324,17 +321,17 @@
 (*Prove the linearity goal first*)
 by (REPEAT (rtac ballI 2));
 by (excluded_middle_tac "x=y" 2);
-by (Fast_tac 3);
+by (Blast_tac 3);
 (*The x~=y case remains*)
 by (res_inst_tac [("n1","x"), ("m1","y")] 
     (TFin_subset_linear RS disjE) 2  THEN  REPEAT (assume_tac 2));
-by (Fast_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
+by (Blast_tac 2);
 (*Now prove the well_foundedness goal*)
 by (rtac wf_onI 1);
 by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
 by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "well_ord_TFin";
 
 (** Defining the "next" operation for Zermelo's Theorem **)
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/equalities.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -532,8 +532,8 @@
 (** RepFun **)
 
 goal ZF.thy "{f(x).x:A}=0 <-> A=0";
-	(*blast_tac takes too long to search depth 5*)
-by (Blast.depth_tac (!claset addSEs [equalityE]) 6 1);
+	(*blast_tac takes too long to find a good depth*)
+by (Blast.depth_tac (!claset addSEs [equalityE]) 10 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/func.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -306,7 +306,8 @@
     "!!S. [| ALL x:S. function(x); \
 \            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
 \         function(Union(S))";
-by (blast_tac (!claset addSDs [bspec RS bspec]) 1);
+by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
+	(*by (Blast_tac 1);  takes too long...*)
 qed "function_Union";
 
 goalw ZF.thy [Pi_def]
@@ -323,13 +324,12 @@
               Un_upper1 RSN (2, subset_trans), 
               Un_upper2 RSN (2, subset_trans)];
 
-goal ZF.thy
-    "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
-\         (f Un g) : (A Un C) -> (B Un D)";
+goal ZF.thy "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |]  \
+\                 ==> (f Un g) : (A Un C) -> (B Un D)";
 (*Prove the product and domain subgoals using distributive laws*)
 by (asm_full_simp_tac (!simpset addsimps [Pi_iff,extension]@Un_rls) 1);
 by (rewtac function_def);
-by (Blast_tac 1);
+by (Blast.depth_tac (!claset) 11 1);	(*11 secs*)
 qed "fun_disjoint_Un";
 
 goal ZF.thy
diff -r af506c35b4ed -r b0ae2e13db93 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/mono.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -13,53 +13,53 @@
 (*Not easy to express monotonicity in P, since any "bigger" predicate
   would have to be single-valued*)
 goal thy "!!A B. A<=B ==> Replace(A,P) <= Replace(B,P)";
-by (fast_tac (!claset addSEs [ReplaceE]) 1);
+by (blast_tac (!claset addSEs [ReplaceE]) 1);
 qed "Replace_mono";
 
 goal thy "!!A B. A<=B ==> {f(x). x:A} <= {f(x). x:B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "RepFun_mono";
 
 goal thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Pow_mono";
 
 goal thy "!!A B. A<=B ==> Union(A) <= Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_mono";
 
 val prems = goal thy
     "[| A<=C;  !!x. x:A ==> B(x)<=D(x) \
 \    |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "UN_mono";
 
 (*Intersection is ANTI-monotonic.  There are TWO premises! *)
 goal thy "!!A B. [| A<=B;  a:A |] ==> Inter(B) <= Inter(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_anti_mono";
 
 goal thy "!!C D. C<=D ==> cons(a,C) <= cons(a,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "cons_mono";
 
 goal thy "!!A B C D. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_mono";
 
 goal thy "!!A B C D. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_mono";
 
 goal thy "!!A B C D. [| A<=C;  D<=B |] ==> A-B <= C-D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_mono";
 
 (** Standard products, sums and function spaces **)
 
 goal thy "!!A B C D. [| A<=C;  ALL x:A. B(x) <= D(x) |] ==> \
 \                       Sigma(A,B) <= Sigma(C,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Sigma_mono_lemma";
 val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
 
@@ -69,7 +69,7 @@
 
 (*Note that B->A and C->A are typically disjoint!*)
 goal thy "!!A B C. B<=C ==> A->B <= A->C";
-by (fast_tac (!claset addIs [lam_type] addEs [Pi_lamE]) 1);
+by (blast_tac (!claset addIs [lam_type] addEs [Pi_lamE]) 1);
 qed "Pi_mono";
 
 goalw thy [lam_def] "!!A B. A<=B ==> Lambda(A,c) <= Lambda(B,c)";
@@ -84,7 +84,7 @@
 
 goal QPair.thy "!!A B C D. [| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
 \                          QSigma(A,B) <= QSigma(C,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "QSigma_mono_lemma";
 val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
 
@@ -97,35 +97,35 @@
 qed "QInr_mono";
 
 goal QPair.thy "!!A B C D. [| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "qsum_mono";
 
 
 (** Converse, domain, range, field **)
 
 goal thy "!!r s. r<=s ==> converse(r) <= converse(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "converse_mono";
 
 goal thy "!!r s. r<=s ==> domain(r)<=domain(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "domain_mono";
 
 bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans);
 
 goal thy "!!r s. r<=s ==> range(r)<=range(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "range_mono";
 
 bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans);
 
 goal thy "!!r s. r<=s ==> field(r)<=field(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "field_mono";
 
 goal thy "!!r A. r <= A*A ==> field(r) <= A";
 by (etac (field_mono RS subset_trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "field_rel_subset";
 
 
@@ -133,31 +133,31 @@
 
 val [prem1,prem2] = goal thy
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B";
-by (fast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
 qed "image_pair_mono";
 
 val [prem1,prem2] = goal thy
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B";
-by (fast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
 qed "vimage_pair_mono";
 
 goal thy "!!r s. [| r<=s;  A<=B |] ==> r``A <= s``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_mono";
 
 goal thy "!!r s. [| r<=s;  A<=B |] ==> r-``A <= s-``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "vimage_mono";
 
 val [sub,PQimp] = goal thy
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
-by (fast_tac (!claset addIs [sub RS subsetD, PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [sub RS subsetD, PQimp RS mp]) 1);
 qed "Collect_mono";
 
 (** Monotonicity of implications -- some could go to FOL **)
 
 goal thy "!!A B x. A<=B ==> x:A --> x:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "in_mono";
 
 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";