# HG changeset patch
# User paulson
# Date 859988192 -7200
# Node ID 6e3ccb94836c07bf4cb7e6c4416f31e70a045ef1
# Parent  b1e7e2179597ee9f7a1969be66dcf4a0326d0e37
Mostly converted to blast_tac

diff -r b1e7e2179597 -r 6e3ccb94836c src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Apr 02 15:30:44 1997 +0200
+++ b/src/ZF/Cardinal.ML	Wed Apr 02 15:36:32 1997 +0200
@@ -45,7 +45,7 @@
     "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
 by (cut_facts_tac prems 1);
 by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
-by (fast_tac (!claset addSIs [restrict_bij,bij_disjoint_Un]
+by (blast_tac (!claset addSIs [restrict_bij,bij_disjoint_Un]
                     addIs [bij_converse_bij]) 1);
 (* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
    is forced by the context!! *)
@@ -62,12 +62,12 @@
 bind_thm ("eqpoll_refl", id_bij RS bij_imp_eqpoll);
 
 goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";
-by (fast_tac (!claset addIs [bij_converse_bij]) 1);
+by (blast_tac (!claset addIs [bij_converse_bij]) 1);
 qed "eqpoll_sym";
 
 goalw Cardinal.thy [eqpoll_def]
     "!!X Y. [| X eqpoll Y;  Y eqpoll Z |] ==> X eqpoll Z";
-by (fast_tac (!claset addIs [comp_bij]) 1);
+by (blast_tac (!claset addIs [comp_bij]) 1);
 qed "eqpoll_trans";
 
 (** Le-pollence is a partial ordering **)
@@ -83,12 +83,12 @@
 
 goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]
     "!!X Y. X eqpoll Y ==> X lepoll Y";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "eqpoll_imp_lepoll";
 
 goalw Cardinal.thy [lepoll_def]
     "!!X Y. [| X lepoll Y;  Y lepoll Z |] ==> X lepoll Z";
-by (fast_tac (!claset addIs [comp_inj]) 1);
+by (blast_tac (!claset addIs [comp_inj]) 1);
 qed "lepoll_trans";
 
 (*Asymmetry law*)
@@ -106,52 +106,52 @@
 qed "eqpollE";
 
 goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X";
-by (fast_tac (!claset addIs [eqpollI] addSEs [eqpollE]) 1);
+by (blast_tac (!claset addIs [eqpollI] addSEs [eqpollE]) 1);
 qed "eqpoll_iff";
 
 goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0";
-by (fast_tac (!claset addDs [apply_type]) 1);
+by (blast_tac (!claset addDs [apply_type]) 1);
 qed "lepoll_0_is_0";
 
 (*0 lepoll Y*)
 bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll);
 
 goal Cardinal.thy "A lepoll 0 <-> A=0";
-by (fast_tac (!claset addIs [lepoll_0_is_0, lepoll_refl]) 1);
+by (blast_tac (!claset addIs [lepoll_0_is_0, lepoll_refl]) 1);
 qed "lepoll_0_iff";
 
 goalw Cardinal.thy [lepoll_def] 
     "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] ==> A Un C lepoll B Un D";
-by (fast_tac (!claset addIs [inj_disjoint_Un]) 1);
+by (blast_tac (!claset addIs [inj_disjoint_Un]) 1);
 qed "Un_lepoll_Un";
 
 (*A eqpoll 0 ==> A=0*)
 bind_thm ("eqpoll_0_is_0",  eqpoll_imp_lepoll RS lepoll_0_is_0);
 
 goal Cardinal.thy "A eqpoll 0 <-> A=0";
-by (fast_tac (!claset addIs [eqpoll_0_is_0, eqpoll_refl]) 1);
+by (blast_tac (!claset addIs [eqpoll_0_is_0, eqpoll_refl]) 1);
 qed "eqpoll_0_iff";
 
 goalw Cardinal.thy [eqpoll_def] 
     "!!A. [| A eqpoll B;  C eqpoll D;  A Int C = 0;  B Int D = 0 |] ==> \
 \         A Un C eqpoll B Un D";
-by (fast_tac (!claset addIs [bij_disjoint_Un]) 1);
+by (blast_tac (!claset addIs [bij_disjoint_Un]) 1);
 qed "eqpoll_disjoint_Un";
 
 
 (*** lesspoll: contributions by Krzysztof Grabczewski ***)
 
 goalw Cardinal.thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "lesspoll_imp_lepoll";
 
 goalw Cardinal.thy [lepoll_def]
         "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
-by (fast_tac (!claset addIs [well_ord_rvimage]) 1);
+by (blast_tac (!claset addIs [well_ord_rvimage]) 1);
 qed "lepoll_well_ord";
 
 goalw Cardinal.thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE]) 1);
+by (blast_tac (!claset addSIs [eqpollI] addSEs [eqpollE]) 1);
 qed "lepoll_iff_leqpoll";
 
 goalw Cardinal.thy [inj_def, surj_def] 
@@ -163,7 +163,7 @@
                       addEs [apply_funtype RS succE]) 1);
 (*Proving it's injective*)
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (fast_tac (!claset delrules [equalityI]) 1);
+by (blast_tac (!claset delrules [equalityI]) 1);
 qed "inj_not_surj_succ";
 
 (** Variations on transitivity **)
@@ -189,10 +189,10 @@
 val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
     "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
 by (rtac the_equality 1);
-by (fast_tac (!claset addSIs [premP,premOrd,premNot]) 1);
+by (blast_tac (!claset addSIs [premP,premOrd,premNot]) 1);
 by (REPEAT (etac conjE 1));
 by (etac (premOrd RS Ord_linear_lt) 1);
-by (ALLGOALS (fast_tac (!claset addSIs [premP] addSDs [premNot])));
+by (ALLGOALS (blast_tac (!claset addSIs [premP] addSDs [premNot])));
 qed "Least_equality";
 
 goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> P(LEAST x.P(x))";
@@ -202,7 +202,7 @@
 by (rtac classical 1);
 by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
 by (assume_tac 2);
-by (fast_tac (!claset addSEs [ltE]) 1);
+by (blast_tac (!claset addSEs [ltE]) 1);
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
@@ -234,7 +234,7 @@
 goalw Cardinal.thy [Least_def]
     "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0";
 by (rtac the_0 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Least_0";
 
 goal Cardinal.thy "Ord(LEAST x.P(x))";
@@ -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 (fast_tac (!claset addEs [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|*)
@@ -282,7 +282,7 @@
 
 goal Cardinal.thy
     "!!X Y. [| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
-by (fast_tac (!claset addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
+by (blast_tac (!claset addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
 qed "well_ord_cardinal_eqpoll_iff";
 
 
@@ -319,7 +319,7 @@
 (*The cardinals are the initial ordinals*)
 goal Cardinal.thy "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j eqpoll K)";
 by (safe_tac (!claset addSIs [CardI, Card_is_Ord]));
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (rewrite_goals_tac [Card_def, cardinal_def]);
 by (rtac less_LeastE 1);
 by (etac subst 2);
@@ -328,12 +328,12 @@
 
 goalw Cardinal.thy [lesspoll_def] "!!a. [| Card(a); i<a |] ==> i lesspoll a";
 by (dresolve_tac [Card_iff_initial RS iffD1] 1);
-by (fast_tac (!claset addSEs [leI RS le_imp_lepoll]) 1);
+by (blast_tac (!claset addSIs [leI RS le_imp_lepoll]) 1);
 qed "lt_Card_imp_lesspoll";
 
 goal Cardinal.thy "Card(0)";
 by (rtac (Ord_0 RS CardI) 1);
-by (fast_tac (!claset addSEs [ltE]) 1);
+by (blast_tac (!claset addSEs [ltE]) 1);
 qed "Card_0";
 
 val [premK,premL] = goal Cardinal.thy
@@ -393,7 +393,7 @@
 qed "Card_lt_imp_lt";
 
 goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)";
-by (fast_tac (!claset addIs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
+by (blast_tac (!claset addIs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
 qed "Card_lt_iff";
 
 goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)";
@@ -438,17 +438,17 @@
 by (rtac CollectI 1);
 (*Proving it's in the function space A->B*)
 by (rtac (if_type RS lam_type) 1);
-by (fast_tac (!claset addEs [apply_funtype RS consE]) 1);
-by (fast_tac (!claset addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1);
+by (blast_tac (!claset addEs [apply_funtype RS consE]) 1);
+by (blast_tac (!claset addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1);
 (*Proving it's injective*)
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "cons_lepoll_consD";
 
 goal Cardinal.thy
  "!!A B. [| cons(u,A) eqpoll cons(v,B);  u~:A;  v~:B |] ==> A eqpoll B";
 by (asm_full_simp_tac (!simpset addsimps [eqpoll_iff]) 1);
-by (fast_tac (!claset addIs [cons_lepoll_consD]) 1);
+by (blast_tac (!claset addIs [cons_lepoll_consD]) 1);
 qed "cons_eqpoll_consD";
 
 (*Lemma suggested by Mike Fourman*)
@@ -460,12 +460,12 @@
 val [prem] = goal Cardinal.thy
     "m:nat ==> ALL n: nat. m lepoll n --> m le n";
 by (nat_ind_tac "m" [prem] 1);
-by (fast_tac (!claset addSIs [nat_0_le]) 1);
+by (blast_tac (!claset addSIs [nat_0_le]) 1);
 by (rtac ballI 1);
 by (eres_inst_tac [("n","n")] natE 1);
 by (asm_simp_tac (!simpset addsimps [lepoll_def, inj_def, 
                                   succI1 RS Pi_empty2]) 1);
-by (fast_tac (!claset addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
+by (blast_tac (!claset addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
 qed "nat_lepoll_imp_le_lemma";
 
 bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
@@ -474,7 +474,7 @@
     "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
 by (rtac iffI 1);
 by (asm_simp_tac (!simpset addsimps [eqpoll_refl]) 2);
-by (fast_tac (!claset addIs [nat_lepoll_imp_le, le_anti_sym] 
+by (blast_tac (!claset addIs [nat_lepoll_imp_le, le_anti_sym] 
                     addSEs [eqpollE]) 1);
 qed "nat_eqpoll_iff";
 
@@ -484,7 +484,7 @@
 by (stac Least_equality 1);
 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
 by (asm_simp_tac (!simpset addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
-by (fast_tac (!claset addSEs [lt_irrefl]) 1);
+by (blast_tac (!claset addSEs [lt_irrefl]) 1);
 qed "nat_into_Card";
 
 (*Part of Kunen's Lemma 10.6*)
@@ -499,7 +499,7 @@
 goalw Cardinal.thy [lesspoll_def]
       "!!m. [| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
 by (rtac conjI 1);
-by (fast_tac (!claset addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
+by (blast_tac (!claset addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
 by (rtac notI 1);
 by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1);
 by (dtac lepoll_trans 1 THEN assume_tac 1);
@@ -509,11 +509,11 @@
 goalw Cardinal.thy [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
       "!!m. [| A lesspoll succ(m); m:nat |] ==> A lepoll m";
 by (step_tac (!claset) 1);
-by (fast_tac (!claset addSIs [inj_not_surj_succ]) 1);
+by (blast_tac (!claset addSIs [inj_not_surj_succ]) 1);
 qed "lesspoll_succ_imp_lepoll";
 
 goal Cardinal.thy "!!m. m:nat ==> A lesspoll succ(m) <-> A lepoll m";
-by (fast_tac (!claset addSIs [lepoll_imp_lesspoll_succ, 
+by (blast_tac (!claset addSIs [lepoll_imp_lesspoll_succ, 
                             lesspoll_succ_imp_lepoll]) 1);
 qed "lesspoll_succ_iff";
 
@@ -586,17 +586,17 @@
 goal Cardinal.thy
     "!!A B. [| a ~: A;  b ~: B |] ==> \
 \           cons(a,A) lepoll cons(b,B)  <->  A lepoll B";
-by (fast_tac (!claset addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
+by (blast_tac (!claset addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
 qed "cons_lepoll_cons_iff";
 
 goal Cardinal.thy
     "!!A B. [| a ~: A;  b ~: B |] ==> \
 \           cons(a,A) eqpoll cons(b,B)  <->  A eqpoll B";
-by (fast_tac (!claset addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
+by (blast_tac (!claset addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
 qed "cons_eqpoll_cons_iff";
 
 goalw Cardinal.thy [succ_def] "{a} eqpoll 1";
-by (fast_tac (!claset addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1);
+by (blast_tac (!claset addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1);
 qed "singleton_eqpoll_1";
 
 goal Cardinal.thy "|{a}| = 1";
@@ -613,13 +613,13 @@
 (*Congruence law for + under equipollence*)
 goalw Cardinal.thy [eqpoll_def]
     "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A+B eqpoll C+D";
-by (fast_tac (!claset addSIs [sum_bij]) 1);
+by (blast_tac (!claset addSIs [sum_bij]) 1);
 qed "sum_eqpoll_cong";
 
 (*Congruence law for * under equipollence*)
 goalw Cardinal.thy [eqpoll_def]
     "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A*B eqpoll C*D";
-by (fast_tac (!claset addSIs [prod_bij]) 1);
+by (blast_tac (!claset addSIs [prod_bij]) 1);
 qed "prod_eqpoll_cong";
 
 goalw Cardinal.thy [eqpoll_def]
@@ -628,7 +628,7 @@
 by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"),
                   ("d", "%y. if(y: range(f), converse(f)`y, y)")] 
     lam_bijective 1);
-by (fast_tac (!claset addSIs [if_type, apply_type] addIs [inj_is_fun]) 1);
+by (blast_tac (!claset addSIs [if_type, inj_is_fun RS apply_type]) 1);
 by (asm_simp_tac 
     (!simpset addsimps [inj_converse_fun RS apply_funtype]
            setloop split_tac [expand_if]) 1);
@@ -637,7 +637,7 @@
 by (asm_simp_tac 
     (!simpset addsimps [inj_converse_fun RS apply_funtype, right_inverse]
            setloop split_tac [expand_if]) 1);
-by (fast_tac (!claset addEs [equals0D]) 1);
+by (blast_tac (!claset addEs [equals0D]) 1);
 qed "inj_disjoint_eqpoll";
 
 
@@ -658,12 +658,12 @@
       "!!A a n. [| succ(n) lepoll A |] ==> n lepoll A - {a}";
 by (rtac cons_lepoll_consD 1);
 by (rtac mem_not_refl 2);
-by (Fast_tac 2);
-by (fast_tac (!claset addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
+by (Blast_tac 2);
+by (blast_tac (!claset addIs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
 qed "lepoll_Diff_sing";
 
 goal Cardinal.thy "!!A a n. [| a:A; A eqpoll succ(n) |] ==> A - {a} eqpoll n";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] 
+by (blast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] 
                     addIs [Diff_sing_lepoll,lepoll_Diff_sing]) 1);
 qed "Diff_sing_eqpoll";
 
@@ -671,14 +671,14 @@
 by (forward_tac [Diff_sing_lepoll] 1);
 by (assume_tac 1);
 by (dtac lepoll_0_is_0 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 qed "lepoll_1_is_sing";
 
 goalw Cardinal.thy [lepoll_def] "A Un B lepoll A+B";
 by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
 by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
 by (split_tac [expand_if] 1);
-by (fast_tac (!claset addSIs [InlI, InrI]) 1);
+by (blast_tac (!claset addSIs [InlI, InrI]) 1);
 by (asm_full_simp_tac (!simpset addsimps [Inl_def, Inr_def]
                        setloop split_tac [expand_if]) 1);
 qed "Un_lepoll_sum";
@@ -687,22 +687,23 @@
 (*** Finite and infinite sets ***)
 
 goalw Cardinal.thy [Finite_def] "Finite(0)";
-by (fast_tac (!claset addSIs [eqpoll_refl, nat_0I]) 1);
+by (blast_tac (!claset addSIs [eqpoll_refl, nat_0I]) 1);
 qed "Finite_0";
 
 goalw Cardinal.thy [Finite_def]
     "!!A. [| A lepoll n;  n:nat |] ==> Finite(A)";
 by (etac rev_mp 1);
 by (etac nat_induct 1);
-by (fast_tac (!claset addSDs [lepoll_0_is_0] addSIs [eqpoll_refl,nat_0I]) 1);
-by (fast_tac (!claset addSDs [lepoll_succ_disj] addSIs [nat_succI]) 1);
+by (blast_tac (!claset addSDs [lepoll_0_is_0] addSIs [eqpoll_refl,nat_0I]) 1);
+by (blast_tac (!claset addSDs [lepoll_succ_disj] addSIs [nat_succI]) 1);
 qed "lepoll_nat_imp_Finite";
 
 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);
+                      addEs [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);
@@ -727,12 +728,12 @@
       "!!i. [| Ord(i);  ~ Finite(i) |] ==> nat le i";
 by (eresolve_tac [Ord_nat RSN (2,Ord_linear2)] 1);
 by (assume_tac 2);
-by (fast_tac (!claset addSIs [eqpoll_refl] addSEs [ltE]) 1);
+by (blast_tac (!claset addSIs [eqpoll_refl] addSEs [ltE]) 1);
 qed "nat_le_infinite_Ord";
 
 goalw Cardinal.thy [Finite_def, eqpoll_def]
     "!!A. Finite(A) ==> EX r. well_ord(A,r)";
-by (fast_tac (!claset addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, 
+by (blast_tac (!claset addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, 
                            nat_into_Ord]) 1);
 qed "Finite_imp_well_ord";
 
@@ -742,22 +743,20 @@
 
 goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
 by (etac nat_induct 1);
-by (fast_tac (!claset addIs [wf_onI]) 1);
+by (blast_tac (!claset addIs [wf_onI]) 1);
 by (rtac wf_onI 1);
 by (asm_full_simp_tac (!simpset addsimps [wf_on_def, wf_def, Memrel_iff]) 1);
 by (excluded_middle_tac "x:Z" 1);
 by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
 by (fast_tac (!claset addSEs [mem_irrefl] addEs [mem_asym]) 2);
 by (dres_inst_tac [("x", "Z")] spec 1);
-by (safe_tac (!claset));
-by (dres_inst_tac [("x", "xa")] bspec 1 THEN assume_tac 1);
-by (Fast_tac 1);
+by (Blast.depth_tac (!claset) 4 1);
 qed "nat_wf_on_converse_Memrel";
 
 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 (fast_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
@@ -778,12 +777,12 @@
     REPEAT (assume_tac 1));
 by (rtac eqpoll_trans 1 THEN assume_tac 2);
 by (rewtac eqpoll_def);
-by (fast_tac (!claset addSIs [ordermap_bij RS bij_converse_bij]) 1);
+by (blast_tac (!claset addSIs [ordermap_bij RS bij_converse_bij]) 1);
 qed "ordertype_eq_n";
 
 goalw Cardinal.thy [Finite_def]
     "!!A. [| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))";
 by (rtac well_ord_converse 1 THEN assume_tac 1);
-by (fast_tac (!claset addDs [ordertype_eq_n] 
+by (blast_tac (!claset addDs [ordertype_eq_n] 
                     addSIs [nat_well_ord_converse_Memrel]) 1);
 qed "Finite_well_ord_converse";
diff -r b1e7e2179597 -r 6e3ccb94836c src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Wed Apr 02 15:30:44 1997 +0200
+++ b/src/ZF/ex/Mutil.ML	Wed Apr 02 15:36:32 1997 +0200
@@ -12,11 +12,11 @@
 (** Basic properties of evnodd **)
 
 goalw thy [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "evnodd_iff";
 
 goalw thy [evnodd_def] "evnodd(A, b) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "evnodd_subset";
 
 (* Finite(X) ==> Finite(evnodd(X,b)) *)
@@ -46,7 +46,7 @@
 (*** Dominoes ***)
 
 goal thy "!!d. d:domino ==> Finite(d)";
-by (fast_tac (!claset addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
+by (blast_tac (!claset addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
 qed "domino_Finite";
 
 goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}";
@@ -57,7 +57,7 @@
 (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
 by (REPEAT (asm_simp_tac (!simpset addsimps [mod_succ, succ_neq_self] 
                                    setloop split_tac [expand_if]) 1
-           THEN fast_tac (!claset addDs [ltD]) 1));
+           THEN blast_tac (!claset addDs [ltD]) 1));
 qed "domino_singleton";
 
 
@@ -69,15 +69,15 @@
 \              u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)";
 by (etac tiling.induct 1);
 by (simp_tac (!simpset addsimps tiling.intrs) 1);
-by (fast_tac (!claset addIs tiling.intrs
-                     addss (!simpset addsimps [Un_assoc,
-                                            subset_empty_iff RS iff_sym])) 1);
+by (asm_full_simp_tac (!simpset addsimps [Un_assoc,
+					  subset_empty_iff RS iff_sym]) 1);
+by (fast_tac (!claset addIs tiling.intrs) 1);
 bind_thm ("tiling_UnI", result() RS mp RS mp);
 
 goal thy "!!t. t:tiling(domino) ==> Finite(t)";
 by (eresolve_tac [tiling.induct] 1);
 by (resolve_tac [Finite_0] 1);
-by (fast_tac (!claset addIs [domino_Finite, Finite_Un]) 1);
+by (blast_tac (!claset addSIs [Finite_Un] addIs [domino_Finite]) 1);
 qed "tiling_domino_Finite";
 
 goal thy "!!t. t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|";
@@ -92,7 +92,7 @@
 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
                                   evnodd_subset RS subset_Finite,
                                   Finite_imp_cardinal_cons]) 1);
-by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
 qed "tiling_domino_0_1";
 
 goal thy "!!i n. [| i: nat;  n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
@@ -103,16 +103,16 @@
 by (assume_tac 2);
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (!claset addEs [mem_irrefl, mem_asym]) 1);
+by (blast_tac (!claset addEs [mem_irrefl, mem_asym]) 1);
 qed "dominoes_tile_row";
 
 goal thy "!!m n. [| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
 by (nat_ind_tac "m" [] 1);
 by (simp_tac (!simpset addsimps tiling.intrs) 1);
 by (asm_simp_tac (!simpset addsimps [Sigma_succ1]) 1);
-by (fast_tac (!claset addIs [tiling_UnI, dominoes_tile_row] 
+by (blast_tac (!claset addIs [tiling_UnI, dominoes_tile_row] 
                     addEs [mem_irrefl]) 1);
 qed "dominoes_tile_matrix";