# HG changeset patch
# User paulson
# Date 861785662 -7200
# Node ID 15763781afb07c81d52041fe0e24856f4c6c1ae8
# Parent  65778b9d865fb705853be774adeb136bc1dd1f1d
Conversion to use blast_tac

diff -r 65778b9d865f -r 15763781afb0 src/ZF/AC.ML
--- a/src/ZF/AC.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/AC.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -12,9 +12,9 @@
 val [nonempty] = goal AC.thy
      "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
 by (excluded_middle_tac "A=0" 1);
-by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Fast_tac 2);
+by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
 (*The non-trivial case*)
-by (fast_tac (!claset addIs [AC, nonempty]) 1);
+by (blast_tac (!claset addIs [AC, nonempty]) 1);
 qed "AC_Pi";
 
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
@@ -27,7 +27,7 @@
 goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
 by (etac exI 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "AC_Pi_Pow";
 
 val [nonempty] = goal AC.thy
@@ -35,12 +35,12 @@
 \     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
 by (etac nonempty 1);
-by (fast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
+by (blast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
 qed "AC_func";
 
 goal ZF.thy "!!x A. [| 0 ~: A;  x: A |] ==> EX y. y:x";
 by (subgoal_tac "x ~= 0" 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "non_empty_family";
 
 goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
@@ -53,7 +53,7 @@
 by (rtac bexI 2);
 by (assume_tac 2);
 by (etac fun_weaken_type 2);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "AC_func_Pow";
 
 goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Arith.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -51,7 +51,7 @@
 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 *)
@@ -428,7 +428,7 @@
 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";
@@ -483,7 +483,7 @@
 \        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*)
@@ -586,7 +586,7 @@
 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);
@@ -594,6 +594,6 @@
 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";
 
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Cardinal.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -159,8 +159,8 @@
 by (safe_tac (claset_of"ZF"));
 by (swap_res_tac [exI] 1);
 by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1);
-by (fast_tac (!claset addSIs [if_type RS lam_type]
-                      addEs [apply_funtype RS succE]) 1);
+by (best_tac (!claset addSIs [if_type RS lam_type]
+                       addEs [apply_funtype RS succE]) 1);
 (*Proving it's injective*)
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (blast_tac (!claset delrules [equalityI]) 1);
@@ -170,17 +170,17 @@
 
 goalw Cardinal.thy [lesspoll_def]
       "!!X. [| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
 qed "lesspoll_trans";
 
 goalw Cardinal.thy [lesspoll_def]
       "!!X. [| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
 qed "lesspoll_lepoll_lesspoll";
 
 goalw Cardinal.thy [lesspoll_def] 
       "!!X. [| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
 qed "lepoll_lesspoll_lesspoll";
 
 
@@ -213,7 +213,7 @@
 by (rtac classical 1);
 by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
 by (etac le_refl 2);
-by (fast_tac (!claset addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
+by (blast_tac (!claset addEs [ltE] addIs [leI, ltI, lt_trans1]) 1);
 qed "Least_le";
 
 (*LEAST really is the smallest*)
@@ -259,7 +259,7 @@
   Converse also requires AC, but see well_ord_cardinal_eqE*)
 goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
 by (rtac Least_cong 1);
-by (blast_tac (!claset addIs [comp_bij,bij_converse_bij]) 1);
+by (blast_tac (!claset addIs [comp_bij, bij_converse_bij]) 1);
 qed "cardinal_cong";
 
 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
@@ -700,10 +700,10 @@
 
 goalw Cardinal.thy [Finite_def]
      "!!X. [| Y lepoll X;  Finite(X) |] ==> Finite(Y)";
-by (fast_tac (!claset addSEs [eqpollE] 
-                      addEs [lepoll_trans RS 
-			     rewrite_rule [Finite_def] 
-			     lepoll_nat_imp_Finite]) 1);
+by (blast_tac 
+    (!claset addSEs [eqpollE] 
+             addIs [lepoll_trans RS 
+		    rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1);
 qed "lepoll_Finite";
 
 bind_thm ("subset_Finite", subset_imp_lepoll RS lepoll_Finite);
@@ -734,7 +734,7 @@
 goalw Cardinal.thy [Finite_def, eqpoll_def]
     "!!A. Finite(A) ==> EX r. well_ord(A,r)";
 by (blast_tac (!claset addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, 
-                           nat_into_Ord]) 1);
+			      nat_into_Ord]) 1);
 qed "Finite_imp_well_ord";
 
 
@@ -756,7 +756,8 @@
 goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))";
 by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
 by (rewtac well_ord_def);
-by (blast_tac (!claset addSIs [tot_ord_converse, nat_wf_on_converse_Memrel]) 1);
+by (blast_tac (!claset addSIs [tot_ord_converse, 
+			       nat_wf_on_converse_Memrel]) 1);
 qed "nat_well_ord_converse_Memrel";
 
 goal Cardinal.thy
@@ -784,5 +785,5 @@
     "!!A. [| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))";
 by (rtac well_ord_converse 1 THEN assume_tac 1);
 by (blast_tac (!claset addDs [ordertype_eq_n] 
-                    addSIs [nat_well_ord_converse_Memrel]) 1);
+                       addSIs [nat_well_ord_converse_Memrel]) 1);
 qed "Finite_well_ord_converse";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/CardinalArith.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -362,7 +362,7 @@
 by (rewtac Card_def);
 by (dtac trans 1);
 by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1);
-by (etac (Ord_succD RS Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1);
+by (etac (Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1);
 by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1));
 qed "InfCard_is_Limit";
 
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Cardinal_AC.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -27,7 +27,7 @@
 qed "cardinal_eqE";
 
 goal Cardinal_AC.thy "|X| = |Y| <-> X eqpoll Y";
-by (fast_tac (!claset addSEs [cardinal_cong, cardinal_eqE]) 1);
+by (blast_tac (!claset addIs [cardinal_cong, cardinal_eqE]) 1);
 qed "cardinal_eqpoll_iff";
 
 goal Cardinal_AC.thy
@@ -93,11 +93,8 @@
 by (etac CollectE 1);
 by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
 by (fast_tac (!claset addSEs [apply_Pair]) 1);
-by (rtac exI 1);
-by (rtac f_imp_injective 1);
-by (rtac Pi_type 1 THEN assume_tac 1);
-by (fast_tac (!claset addDs [apply_type] addDs [Pi_memberD]) 1);
-by (fast_tac (!claset addDs [apply_type] addEs [apply_equality]) 1);
+by (blast_tac (!claset addDs [apply_type, Pi_memberD] 
+                       addIs [apply_equality, Pi_type, f_imp_injective]) 1);
 qed "surj_implies_inj";
 
 (*Kunen's Lemma 10.20*)
@@ -123,14 +120,14 @@
 by (subgoal_tac
     "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
 by (fast_tac (!claset addSIs [Least_le RS lt_trans1 RS ltD, ltI]
-                    addSEs [LeastI, Ord_in_Ord]) 2);
+                      addSEs [LeastI, Ord_in_Ord]) 2);
 by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
                   ("d", "%<i,j>. converse(f`i) ` j")] 
         lam_injective 1);
 (*Instantiate the lemma proved above*)
 by (ALLGOALS ball_tac);
-by (fast_tac (!claset addEs [inj_is_fun RS apply_type]
-                    addDs [apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]
+                       addDs [apply_type]) 1);
 by (dtac apply_type 1);
 by (etac conjunct2 1);
 by (asm_simp_tac (!simpset addsimps [left_inverse]) 1);
@@ -152,8 +149,8 @@
 \         (UN i:K. j(i)) < csucc(K)";
 by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
 by (assume_tac 1);
-by (fast_tac (!claset addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
-by (fast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 1);
+by (blast_tac (!claset addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
+by (blast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 1);
 by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
 qed "cardinal_UN_Ord_lt_csucc";
 
@@ -194,7 +191,7 @@
 by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] 
                   MRS lt_subset_trans] 1);
 by (REPEAT (assume_tac 1));
-by (fast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 2);
+by (blast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 2);
 by (asm_simp_tac (!simpset addsimps [inj_converse_fun RS apply_type]
                         setloop split_tac [expand_if]) 1);
 qed "le_UN_Ord_lt_csucc";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Epsilon.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -66,7 +66,7 @@
 by (etac nat_induct 1);
 by (asm_simp_tac (!simpset addsimps [nat_rec_0]) 1);
 by (asm_simp_tac (!simpset addsimps [nat_rec_succ]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "eclose_least_lemma";
 
 goalw Epsilon.thy [eclose_def]
@@ -86,7 +86,7 @@
 by (etac (arg_subset_eclose RS subsetD) 2);
 by (etac base 2);
 by (rewtac Transset_def);
-by (fast_tac (!claset addEs [step,ecloseD]) 1);
+by (blast_tac (!claset addIs [step,ecloseD]) 1);
 qed "eclose_induct_down";
 
 goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
@@ -112,7 +112,7 @@
 
 goalw Epsilon.thy [Transset_def]
     "!!i j. [| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (blast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
 qed "under_Memrel";
 
 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
@@ -228,14 +228,14 @@
 
 goal Epsilon.thy "rank(0) = 0";
 by (rtac (rank RS trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rank_0";
 
 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
 by (rtac (rank RS trans) 1);
 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
 by (etac succE 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
 qed "rank_succ";
 
@@ -307,22 +307,21 @@
 qed "transrec2_0";
 
 goal thy "(THE j. i=j) = i";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+by (blast_tac (!claset addSIs [the_equality]) 1);
 qed "THE_eq";
 
 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
 by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P]
-                    setSolver K Fast_tac) 1);
+                    setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
 qed "transrec2_succ";
 
 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (resolve_tac [if_not_P RS trans] 1 THEN
-    fast_tac (!claset addSDs [Limit_has_0] addSEs [ltE]) 1);
-by (resolve_tac [if_not_P RS trans] 1 THEN
-    fast_tac (!claset addSEs [succ_LimitE]) 1);
-by (Simp_tac 1);
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (blast_tac (!claset addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
 qed "transrec2_Limit";
 
 Addsimps [transrec2_0, transrec2_succ];
+
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Fixedpt.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -56,13 +56,13 @@
 (*lfp is contained in each pre-fixedpoint*)
 goalw Fixedpt.thy [lfp_def]
     "!!A. [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 (*or  by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
 qed "lfp_lowerbound";
 
 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
 goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "lfp_subset";
 
 (*Used in datatype package*)
@@ -190,7 +190,7 @@
 qed "gfp_upperbound";
 
 goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "gfp_subset";
 
 (*Used in datatype package*)
diff -r 65778b9d865f -r 15763781afb0 src/ZF/List.ML
--- a/src/ZF/List.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/List.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -28,7 +28,7 @@
 
 goal List.thy "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
+by (blast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "list_unfold";
 
@@ -44,7 +44,7 @@
 goalw List.thy (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
-by (fast_tac (!claset addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
+by (blast_tac (!claset addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
                             Pair_in_univ]) 1);
 qed "list_univ";
 
@@ -233,7 +233,7 @@
 goalw List.thy [set_of_list_def] 
     "!!l. l: list(A) ==> set_of_list(l) : Pow(A)";
 by (etac list_rec_type 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
 qed "set_of_list_type";
 
 goal List.thy
@@ -267,19 +267,19 @@
 val prems = goal List.thy
     "l: list(A) ==> map(%u.u, l) = l";
 by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 
 val prems = goal List.thy
     "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
 by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
 
 val prems = goal List.thy
     "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
 by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "map_app_distrib";
 
 val prems = goal List.thy
@@ -293,7 +293,7 @@
 \    list_rec(map(h,l), c, d) = \
 \    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
 by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "list_rec_map";
 
 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
@@ -304,7 +304,7 @@
 val prems = goal List.thy
     "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
 by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "map_list_Collect";
 
 (*** theorems about length ***)
@@ -312,13 +312,13 @@
 val prems = goal List.thy
     "xs: list(A) ==> length(map(h,xs)) = length(xs)";
 by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "length_map";
 
 val prems = goal List.thy
     "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
 by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "length_app";
 
 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
@@ -345,7 +345,7 @@
 \          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "drop_length_Cons_lemma";
 bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
 
@@ -359,12 +359,8 @@
 by (rtac natE 1);
 by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
 by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
-by (Asm_simp_tac 1);
-by (dtac bspec 1);
-by (Fast_tac 2);
-by (fast_tac (!claset addEs [succ_in_naturalD,length_type]) 1);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addIs [succ_in_naturalD, length_type])));
 qed "drop_length_lemma";
 bind_thm ("drop_length", (drop_length_lemma RS bspec));
 
@@ -373,12 +369,12 @@
 
 val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
 by (rtac (major RS list.induct) 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "app_right_Nil";
 
 val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
 by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "app_assoc";
 
 val prems = goal List.thy
diff -r 65778b9d865f -r 15763781afb0 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/OrderArith.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -82,16 +82,12 @@
 by (thin_tac "y : A + B" 2);
 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 (Blast_tac 2);
-by (best_tac (!claset addSEs [raddE]) 2);
+by (best_tac (!claset addSEs [raddE, bspec RS mp]) 2);
 (*Returning to main part of proof*)
 by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
-by (Best_tac 1);
+by (Blast_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 (Blast_tac 1);
-by (best_tac (!claset addSEs [raddE]) 1);
+by (best_tac (!claset addSEs [raddE, bspec RS mp]) 1);
 qed "wf_on_radd";
 
 goal OrderArith.thy
@@ -225,9 +221,7 @@
 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 (Blast_tac 1);
-by (best_tac (!claset addSEs [rmultE]) 1);
+by (best_tac (!claset addSEs [rmultE, bspec RS mp]) 1);
 qed "wf_on_rmult";
 
 
@@ -267,7 +261,7 @@
 by (ALLGOALS
     (asm_full_simp_tac (!simpset addsimps [bij_is_fun RS apply_type])));
 by (Blast_tac 1);
-by (fast_tac (!claset addSEs [bij_is_inj RS inj_apply_equality]) 1);
+by (blast_tac (!claset addIs [bij_is_inj RS inj_apply_equality]) 1);
 qed "prod_ord_iso_cong";
 
 goal OrderArith.thy "(lam z:A. <x,z>) : bij(A, {x}*A)";
@@ -313,8 +307,8 @@
     (!simpset addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
 by (Asm_simp_tac 1);
 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE]));
-by (ALLGOALS (Asm_simp_tac));
-by (ALLGOALS (fast_tac (!claset addEs [well_ord_is_wf RS wf_on_asym])));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addEs [well_ord_is_wf RS wf_on_asym])));
 qed "prod_sum_singleton_ord_iso";
 
 (** Distributive law **)
@@ -334,7 +328,7 @@
 \           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
 by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE]));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
 qed "sum_prod_distrib_ord_iso";
 
 (** Associativity **)
@@ -442,5 +436,5 @@
 
 goalw OrderArith.thy [ord_iso_def, rvimage_def]
     "!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ord_iso_rvimage_eq";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/OrderType.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -155,9 +155,9 @@
 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
 by (fast_tac (!claset addSIs [ordermap_type, ordermap_surj]
-                    addEs [linearE]
-                    addDs [ordermap_mono]
-                    addss (!simpset addsimps [mem_not_refl])) 1);
+                      addEs [linearE]
+                      addDs [ordermap_mono]
+                      addss (!simpset addsimps [mem_not_refl])) 1);
 qed "ordermap_bij";
 
 (*** Isomorphisms involving ordertype ***)
@@ -455,12 +455,12 @@
 by (rtac Ord_linear_lt 1);
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
-    (fast_tac (!claset addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
+    (blast_tac (!claset addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
 qed "oadd_lt_cancel2";
 
 goal OrderType.thy
     "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
-by (fast_tac (!claset addSIs [oadd_lt_mono2] addSEs [oadd_lt_cancel2]) 1);
+by (blast_tac (!claset addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
 qed "oadd_lt_iff2";
 
 goal OrderType.thy
@@ -469,7 +469,7 @@
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
     (fast_tac (!claset addDs [oadd_lt_mono2] 
-                     addss (!simpset addsimps [lt_not_refl]))));
+                       addss (!simpset addsimps [lt_not_refl]))));
 qed "oadd_inject";
 
 goalw OrderType.thy [oadd_def] 
@@ -508,7 +508,7 @@
 by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
 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);
+                      addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
 by (Blast_tac 2);
 by (blast_tac (!claset addSEs [ltE]) 1);
 qed "oadd_unfold";
@@ -667,7 +667,7 @@
 (*** A useful unfolding law ***)
 
 goalw OrderType.thy [pred_def]
- "!!A B. [| a:A;  b:B |] ==>  \
+ "!!A B. [| a:A;  b:B |] ==>                    \
 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
 by (rtac equalityI 1);
@@ -677,9 +677,9 @@
 qed "pred_Pair_eq";
 
 goal OrderType.thy
- "!!A B. [| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
+ "!!A B. [| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>           \
 \        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
-\        ordertype(pred(A,a,r)*B + pred(B,b,s),                 \
+\        ordertype(pred(A,a,r)*B + pred(B,b,s),                        \
 \                 radd(A*B, rmult(A,r,B,s), B, s))";
 by (asm_simp_tac (!simpset addsimps [pred_Pair_eq]) 1);
 by (resolve_tac [ordertype_eq RS sym] 1);
@@ -689,12 +689,12 @@
 qed "ordertype_pred_Pair_eq";
 
 goalw OrderType.thy [oadd_def, omult_def]
- "!!i j. [| i'<i;  j'<j |] ==>  \
+ "!!i j. [| i'<i;  j'<j |] ==>                                         \
 \        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
-\                  rmult(i,Memrel(i),j,Memrel(j))) = \
+\                  rmult(i,Memrel(i),j,Memrel(j))) =                   \
 \        j**i' ++ j'";
 by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
-                                  ltD, lt_Ord2, well_ord_Memrel]) 1);
+				     ltD, lt_Ord2, well_ord_Memrel]) 1);
 by (rtac trans 1);
 by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
 by (rtac ord_iso_refl 3);
@@ -702,10 +702,9 @@
 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
 by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
                             Ord_ordertype]));
-by (ALLGOALS 
-    (asm_simp_tac (!simpset addsimps [rmult_iff, id_conv, Memrel_iff])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Memrel_iff])));
 by (safe_tac (!claset));
-by (ALLGOALS (fast_tac (!claset addEs [Ord_trans])));
+by (ALLGOALS (blast_tac (!claset addIs [Ord_trans])));
 qed "ordertype_pred_Pair_lemma";
 
 goalw OrderType.thy [omult_def]
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Ordinal.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -110,6 +110,8 @@
 (* Ord(succ(j)) ==> Ord(j) *)
 val Ord_succD = succI1 RSN (2, Ord_in_Ord);
 
+AddSDs [Ord_succD];
+
 goal Ordinal.thy "!!i j. [| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)";
 by (REPEAT (ares_tac [OrdI] 1
      ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
@@ -480,8 +482,8 @@
 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);
+by (blast_tac (!claset addDs [Ord_succD, subset_imp_le, le_imp_subset]
+                       addEs [ltE]) 1);
 qed "le_subset_iff";
 
 goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
@@ -513,7 +515,7 @@
 goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
 by (rtac (not_lt_iff_le RS iffD1) 1);
 by (blast_tac le_cs 3);
-by (ALLGOALS (blast_tac (!claset addEs [ltE] addIs [Ord_succ])));
+by (ALLGOALS (blast_tac (!claset addEs [ltE])));
 qed "succ_leI";
 
 (*Identical to  succ(i) < succ(j) ==> i<j  *)
@@ -627,12 +629,12 @@
 qed "le_implies_UN_le_UN";
 
 goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (best_tac (!claset addEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
 qed "Ord_equality";
 
 (*Holds for all transitive sets, not just ordinals*)
 goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
-by (fast_tac (!claset addSEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
 qed "Ord_Union_subset";
 
 
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Perm.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -18,8 +18,7 @@
 qed "surj_is_fun";
 
 goalw Perm.thy [surj_def] "!!f A B. f : Pi(A,B) ==> f: surj(A,range(f))";
-by (fast_tac (!claset addIs [apply_equality] 
-                    addEs [range_of_fun,domain_type]) 1);
+by (blast_tac (!claset addIs [apply_equality, range_of_fun, domain_type]) 1);
 qed "fun_is_surj";
 
 goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B";
@@ -31,7 +30,7 @@
 val prems = goalw Perm.thy [surj_def]
     "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y \
 \    |] ==> f: surj(A,B)";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "f_imp_surjective";
 
 val prems = goal Perm.thy
@@ -61,11 +60,11 @@
 goalw Perm.thy [inj_def]
     "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
 by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "inj_equality";
 
 goalw thy [inj_def] "!!A B f. [| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
-by (Fast_tac 1);
+by (Blast_tac 1);
 val inj_apply_equality = result();
 
 (** A function with a left inverse is an injection **)
@@ -143,15 +142,16 @@
 val id_inj = subset_refl RS id_subset_inj;
 
 goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
-by (fast_tac (!claset addIs [lam_type,beta]) 1);
+by (blast_tac (!claset addIs [lam_type, beta]) 1);
 qed "id_surj";
 
 goalw Perm.thy [bij_def] "id(A): bij(A,A)";
-by (fast_tac (!claset addIs [id_inj,id_surj]) 1);
+by (blast_tac (!claset addIs [id_inj, id_surj]) 1);
 qed "id_bij";
 
 goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B";
-by (fast_tac (!claset addSIs [lam_type] addDs [apply_type] addss (!simpset)) 1);
+by (fast_tac (!claset addSIs [lam_type] addDs [apply_type] 
+                      addss (!simpset)) 1);
 qed "subset_iff_id";
 
 
@@ -161,20 +161,21 @@
 by (asm_simp_tac (!simpset addsimps [Pi_iff, function_def]) 1);
 by (etac CollectE 1);
 by (asm_simp_tac (!simpset addsimps [apply_iff]) 1);
-by (fast_tac (!claset addDs [fun_is_rel]) 1);
+by (blast_tac (!claset addDs [fun_is_rel]) 1);
 qed "inj_converse_fun";
 
 (** Equations for converse(f) **)
 
 (*The premises are equivalent to saying that f is injective...*) 
-val prems = goal Perm.thy
-    "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
-by (fast_tac (!claset addIs (prems@[apply_Pair,apply_equality,converseI])) 1);
+goal Perm.thy
+    "!!f. [| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
+by (blast_tac (!claset addIs [apply_Pair, apply_equality, converseI]) 1);
 qed "left_inverse_lemma";
 
 goal Perm.thy
     "!!f. [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
-by (fast_tac (!claset addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1);
+by (blast_tac (!claset addIs [left_inverse_lemma, inj_converse_fun,
+			      inj_is_fun]) 1);
 qed "left_inverse";
 
 val left_inverse_bij = bij_is_inj RS left_inverse;
@@ -210,14 +211,13 @@
 qed "inj_converse_inj";
 
 goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
-by (ITER_DEEPEN (has_fewer_prems 1)
-    (ares_tac [f_imp_surjective, inj_converse_fun, left_inverse,
-               inj_is_fun, range_of_fun RS apply_type]));
+by (blast_tac (!claset addIs [f_imp_surjective, inj_converse_fun, left_inverse,
+			      inj_is_fun, range_of_fun RS apply_type]) 1);
 qed "inj_converse_surj";
 
 goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
 by (fast_tac (!claset addEs [surj_range RS subst, inj_converse_inj,
-                           inj_converse_surj]) 1);
+			      inj_converse_surj]) 1);
 qed "bij_converse_bij";
 (*Adding this as an SI seems to cause looping*)
 
@@ -227,7 +227,7 @@
 (*The inductive definition package could derive these theorems for (r O s)*)
 
 goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "compI";
 
 val prems = goalw Perm.thy [comp_def]
@@ -251,56 +251,56 @@
 
 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
 goal Perm.thy "range(r O s) <= range(r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "range_comp";
 
 goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)";
 by (rtac (range_comp RS equalityI) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "range_comp_eq";
 
 goal Perm.thy "domain(r O s) <= domain(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "domain_comp";
 
 goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)";
 by (rtac (domain_comp RS equalityI) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "domain_comp_eq";
 
 goal Perm.thy "(r O s)``A = r``(s``A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_comp";
 
 
 (** Other results **)
 
 goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_mono";
 
 (*composition preserves relations*)
 goal Perm.thy "!!r s. [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_rel";
 
 (*associative law for composition*)
 goal Perm.thy "(r O s) O t = r O (s O t)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_assoc";
 
 (*left identity of composition; provable inclusions are
         id(A) O r <= r       
   and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
 goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "left_comp_id";
 
 (*right identity of composition; provable inclusions are
         r O id(A) <= r
   and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
 goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "right_comp_id";
 
 
@@ -308,7 +308,7 @@
 
 goalw Perm.thy [function_def]
     "!!f g. [| function(g);  function(f) |] ==> function(f O g)";
-by (fast_tac (!claset addIs [compI] addSEs [compE, Pair_inject]) 1);
+by (Blast_tac 1);
 qed "comp_function";
 
 goal Perm.thy "!!f g. [| g: A->B;  f: B->C |] ==> (f O g) : A->C";
@@ -316,7 +316,7 @@
     (!simpset addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
            setloop etac conjE) 1);
 by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_fun";
 
 goal Perm.thy "!!f g. [| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
@@ -348,12 +348,12 @@
 
 goalw Perm.thy [surj_def]
     "!!f g. [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
-by (best_tac (!claset addSIs [comp_fun,comp_fun_apply]) 1);
+by (blast_tac (!claset addSIs [comp_fun,comp_fun_apply]) 1);
 qed "comp_surj";
 
 goalw Perm.thy [bij_def]
     "!!f g. [| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
-by (fast_tac (!claset addIs [comp_inj,comp_surj]) 1);
+by (blast_tac (!claset addIs [comp_inj,comp_surj]) 1);
 qed "comp_bij";
 
 
@@ -382,7 +382,7 @@
 
 goalw Perm.thy [surj_def]
     "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
-by (best_tac (!claset addSIs [comp_fun_apply RS sym, apply_type]) 1);
+by (blast_tac (!claset addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
 qed "comp_mem_surjD1";
 
 goal Perm.thy
@@ -395,7 +395,7 @@
 by (safe_tac (!claset));
 by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
 by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
-by (best_tac (!claset addSIs [apply_type]) 1);
+by (blast_tac (!claset addSIs [apply_funtype]) 1);
 qed "comp_mem_surjD2";
 
 
@@ -418,7 +418,7 @@
 by (cut_facts_tac [prem] 1);
 by (rtac equalityI 1);
 by (best_tac (!claset addEs [domain_type, range_type, make_elim appfD]) 1);
-by (best_tac (!claset addIs [apply_Pair]) 1);
+by (blast_tac (!claset addIs [apply_Pair]) 1);
 qed "right_comp_inverse";
 
 (** Proving that a function is a bijection **)
@@ -462,16 +462,14 @@
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [inj_is_fun RS apply_type, left_inverse] 
                          setloop (split_tac [expand_if] ORELSE' etac UnE))));
-by (fast_tac (!claset addSEs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
 qed "inj_disjoint_Un";
 
 goalw Perm.thy [surj_def]
     "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
 \           (f Un g) : surj(A Un C, B Un D)";
-by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1
-            ORELSE ball_tac 1
-            ORELSE (rtac trans 1 THEN atac 2)
-            ORELSE step_tac (!claset addIs [fun_disjoint_Un]) 1));
+by (blast_tac (!claset addIs [fun_disjoint_apply1, fun_disjoint_apply2,
+			      fun_disjoint_Un, trans]) 1);
 qed "surj_disjoint_Un";
 
 (*A simple, high-level proof; the version for injections follows from it,
@@ -517,23 +515,21 @@
 
 goalw Perm.thy [inj_def,bij_def]
     "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
-by (safe_tac (!claset));
-by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD,
-                          box_equals, restrict] 1
-     ORELSE ares_tac [surj_is_fun,restrict_surj] 1));
+by (blast_tac (!claset addSIs [restrict, restrict_surj]
+		       addIs [box_equals, surj_is_fun]) 1);
 qed "restrict_bij";
 
 
 (*** Lemmas for Ramsey's Theorem ***)
 
 goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B);  B<=D |] ==> f: inj(A,D)";
-by (fast_tac (!claset addSEs [fun_weaken_type]) 1);
+by (blast_tac (!claset addIs [fun_weaken_type]) 1);
 qed "inj_weaken_type";
 
 val [major] = goal Perm.thy  
     "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
 by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (cut_facts_tac [major] 1);
 by (rewtac inj_def);
 by (fast_tac (!claset addEs [range_type, mem_irrefl] 
@@ -543,8 +539,8 @@
 goalw Perm.thy [inj_def]
     "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
 \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
-by (fast_tac (!claset  addIs [apply_type]
-              unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
-                                            fun_extend_apply1]) ) 1);
+by (fast_tac (!claset addIs [apply_type]
+               unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+						fun_extend_apply1])) 1);
 qed "inj_extend";
 
diff -r 65778b9d865f -r 15763781afb0 src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/QPair.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -51,7 +51,7 @@
 
 qed_goalw "QSigmaI" thy [QSigma_def]
     "!!A B. [| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
 AddSIs [QSigmaI];
 
@@ -88,10 +88,10 @@
  (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
 
 qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [QSigma_empty1, QSigma_empty2];
 
@@ -100,11 +100,11 @@
 
 qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
  (fn _=> 
-  [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+  [ (blast_tac (!claset addIs [the_equality]) 1) ]);
 
 qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
  (fn _=> 
-  [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+  [ (blast_tac (!claset addIs [the_equality]) 1) ]);
 
 Addsimps [qfst_conv, qsnd_conv];
 
@@ -171,11 +171,11 @@
 
 qed_goalw "qconverseI" thy [qconverse_def]
     "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goalw "qconverseD" thy [qconverse_def]
     "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goalw "qconverseE" thy [qconverse_def]
     "[| yx : qconverse(r);  \
@@ -192,17 +192,17 @@
 
 qed_goal "qconverse_qconverse" thy
     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "qconverse_type" thy
     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "qconverse_empty" thy "qconverse(0) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 
 (**** The Quine-inspired notion of disjoint sum ****)
@@ -212,11 +212,11 @@
 (** Introduction rules for the injections **)
 
 goalw thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "QInlI";
 
 goalw thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "QInrI";
 
 (** Elimination rules **)
@@ -267,27 +267,27 @@
 Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
 
 goal thy "!!A B. QInl(a): A<+>B ==> a: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "QInlD";
 
 goal thy "!!A B. QInr(b): A<+>B ==> b: B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "QInrD";
 
 (** <+> is itself injective... who cares?? **)
 
 goal thy
     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "qsum_iff";
 
 goal thy "A <+> B <= C <+> D <-> A<=C & B<=D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "qsum_subset_iff";
 
 goal thy "A <+> B = C <+> D <-> A=C & B=D";
 by (simp_tac (!simpset addsimps [extension,qsum_subset_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "qsum_equal_iff";
 
 (*** Eliminator -- qcase ***)
@@ -315,17 +315,17 @@
 (** Rules for the Part primitive **)
 
 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_QInl";
 
 goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_QInr";
 
 goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_QInr2";
 
 goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_qsum_equality";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/QUniv.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -20,7 +20,7 @@
 val [prem] = goalw QUniv.thy [sum_def]
     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
 by (stac Int_Un_distrib 1);
-by (fast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
 qed "Transset_sum_Int_subset";
 
 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
@@ -187,13 +187,13 @@
 goalw Univ.thy [Pair_def]
     "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
 \         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
-by (fast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
+by (blast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
 qed "Pair_in_Vfrom_D";
 
 goal Univ.thy
  "!!X. Transset(X) ==>          \
 \      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (fast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
+by (blast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
 qed "product_Int_Vfrom_subset";
 
 (*** Intersecting <a;b> with Vfrom... ***)
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Rel.ML
--- a/src/ZF/Rel.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Rel.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -30,7 +30,7 @@
 qed "symI";
 
 goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |]  ==>  <y,x>: r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "symE";
 
 (* antisymmetry *)
@@ -43,18 +43,18 @@
 
 val prems = goalw Rel.thy [antisym_def]
      "!!r. [| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "antisymE";
 
 (* transitivity *)
 
 goalw Rel.thy [trans_def]
     "!!r. [| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "transD";
 
 goalw Rel.thy [trans_on_def]
     "!!r. [| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "trans_onD";
 
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Trancl.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -68,7 +68,7 @@
 \     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
 \  ==>  P(<a,b>)";
 by (rtac ([rtrancl_def, rtrancl_bnd_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "rtrancl_full_induct";
 
 (*nice induction rule.
@@ -85,7 +85,7 @@
 by (EVERY1 [etac (spec RS mp), rtac refl]);
 (*now do the induction*)
 by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
 qed "rtrancl_induct";
 
 (*transitivity of transitive closure!! -- by induction.*)
@@ -111,33 +111,30 @@
 
 (*Transitivity of r^+ is proved by transitivity of r^*  *)
 goalw Trancl.thy [trans_def,trancl_def] "trans(r^+)";
-by (safe_tac (!claset));
-by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
-by (REPEAT (assume_tac 1));
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl RS 
+			      (trans_rtrancl RS transD RS compI)]) 1);
 qed "trans_trancl";
 
 (** Conversions between trancl and rtrancl **)
 
-val [major] = goalw Trancl.thy [trancl_def] "<a,b> : r^+ ==> <a,b> : r^*";
-by (resolve_tac [major RS compEpair] 1);
-by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
+goalw Trancl.thy [trancl_def] "!!r. <a,b> : r^+ ==> <a,b> : r^*";
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1);
 qed "trancl_into_rtrancl";
 
 (*r^+ contains all pairs in r  *)
-val [prem] = goalw Trancl.thy [trancl_def] "<a,b> : r ==> <a,b> : r^+";
-by (REPEAT (ares_tac [prem,compI,rtrancl_refl,fieldI1] 1));
+goalw Trancl.thy [trancl_def] "!!r. <a,b> : r ==> <a,b> : r^+";
+by (blast_tac (!claset addSIs [rtrancl_refl]) 1);
 qed "r_into_trancl";
 
 (*The premise ensures that r consists entirely of pairs*)
-val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^+";
-by (cut_facts_tac prems 1);
+goal Trancl.thy "!!r. r <= Sigma(A,B) ==> r <= r^+";
 by (blast_tac (!claset addIs [r_into_trancl]) 1);
 qed "r_subset_trancl";
 
 (*intro rule by definition: from r^* and r  *)
-val prems = goalw Trancl.thy [trancl_def]
-    "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
-by (REPEAT (resolve_tac ([compI]@prems) 1));
+goalw Trancl.thy [trancl_def]
+    "!!r. [| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
+by (Blast_tac 1);
 qed "rtrancl_into_trancl1";
 
 (*intro rule from r and r^*  *)
diff -r 65778b9d865f -r 15763781afb0 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Univ.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -618,9 +618,7 @@
 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);
+by (blast_tac (!claset addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
 val Fin_Vfrom_lemma = result();
 
 goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
diff -r 65778b9d865f -r 15763781afb0 src/ZF/WF.ML
--- a/src/ZF/WF.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/WF.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -25,7 +25,7 @@
 (** Equivalences between wf and wf_on **)
 
 goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_imp_wf_on";
 
 goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
@@ -33,7 +33,7 @@
 qed "wf_on_field_imp_wf";
 
 goal WF.thy "wf(r) <-> wf[field(r)](r)";
-by (fast_tac (!claset addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
+by (blast_tac (!claset addIs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
 qed "wf_iff_wf_on_field";
 
 goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
@@ -52,7 +52,7 @@
 \    ==>  wf[A](r)";
 by (rtac (equals0I RS disjCI RS allI) 1);
 by (res_inst_tac [ ("Z", "Z") ] prem 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "wf_onI";
 
 (*If r allows well-founded induction over A then wf[A](r)
@@ -65,7 +65,7 @@
 by (rtac wf_onI 1);
 by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
 by (contr_tac 3);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (Fast_tac 1);
 qed "wf_onI2";
 
@@ -79,9 +79,9 @@
 \    |]  ==>  P(a)";
 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
 by (etac disjE 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 by (asm_full_simp_tac (!simpset addsimps [domainI]) 1);
-by (fast_tac (!claset addSDs [minor]) 1);
+by (blast_tac (!claset addSDs [minor]) 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -99,11 +99,11 @@
 by (wf_ind_tac "a" [wfr] 1);
 by (rtac impI 1);
 by (eresolve_tac prems 1);
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "wf_induct2";
 
 goal domrange.thy "!!r A. field(r Int A*A) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "field_Int_square";
 
 val wfr::amem::prems = goalw WF.thy [wf_on_def]
@@ -112,7 +112,7 @@
 \    |]  ==>  P(a)";
 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
 by (REPEAT (ares_tac prems 1));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_induct";
 
 fun wf_on_ind_tac a prems i = 
@@ -135,26 +135,26 @@
 
 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
 by (wf_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_not_refl";
 
 goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
 by (wf_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_asym";
 
 goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
 by (wf_on_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_not_refl";
 
 goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
 by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
 by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_on_asym";
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
@@ -164,8 +164,8 @@
 by (subgoal_tac
     "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
 by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_on_chain3";
 
 
@@ -178,20 +178,15 @@
 by (rtac wf_onI2 1);
 by (bchain_tac 1);
 by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
-by (rtac (impI RS ballI) 1);
-by (etac tranclE 1);
-by (etac (bspec RS mp) 1 THEN assume_tac 1);
-by (Fast_tac 1);
 by (cut_facts_tac [subs] 1);
-(*astar_tac is slightly faster*)
-by (Best_tac 1);
+by (blast_tac (!claset addEs [tranclE]) 1);
 qed "wf_on_trancl";
 
 goal WF.thy "!!r. wf(r) ==> wf(r^+)";
 by (asm_full_simp_tac (!simpset addsimps [wf_iff_wf_on_field]) 1);
 by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
 by (etac wf_on_trancl 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_trancl";