# HG changeset patch
# User paulson
# Date 860145532 -7200
# Node ID d8f254ad1ab9a9af0311a5a3b6b69689a7573413
# Parent  f27002fc531dff8bbbf4b98bf2d1239c26791180
Calls Blast_tac

diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -37,20 +37,20 @@
 (**** keysFor operator ****)
 
 goalw thy [keysFor_def] "keysFor {} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "keysFor_empty";
 
 goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "keysFor_Un";
 
 goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "keysFor_UN";
 
 (*Monotonicity*)
 goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "keysFor_mono";
 
 goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
@@ -83,7 +83,7 @@
           keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
 
 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Crypt_imp_invKey_keysFor";
 
 
@@ -108,7 +108,7 @@
      proofs concern only atomic messages.*)
 
 goal thy "H <= parts(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "parts_increasing";
 
 (*Monotonicity*)
@@ -122,7 +122,7 @@
 goal thy "parts{} = {}";
 by (Step_tac 1);
 by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "parts_empty";
 Addsimps [parts_empty];
 
@@ -134,7 +134,7 @@
 (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
 goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
 by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "parts_singleton";
 
 
@@ -147,7 +147,7 @@
 goal thy "parts(G Un H) <= parts(G) Un parts(H)";
 by (rtac subsetI 1);
 by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 val parts_Un_subset2 = result();
 
 goal thy "parts(G Un H) = parts(G) Un parts(H)";
@@ -173,7 +173,7 @@
 goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
 by (rtac subsetI 1);
 by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 val parts_UN_subset2 = result();
 
 goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
@@ -195,18 +195,18 @@
 
 goal thy "!!H. X: parts (parts H) ==> X: parts H";
 by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "parts_partsE";
-AddSEs [parts_partsE];
+AddSDs [parts_partsE];
 
 goal thy "parts (parts H) = parts H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "parts_idem";
 Addsimps [parts_idem];
 
 goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
 by (dtac parts_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "parts_trans";
 
 (*Cut*)
@@ -299,13 +299,13 @@
 Addsimps [analz.Inj];
 
 goal thy "H <= analz(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "analz_increasing";
 
 goal thy "analz H <= parts H";
 by (rtac subsetI 1);
 by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "analz_subset_parts";
 
 bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
@@ -315,7 +315,7 @@
 by (rtac equalityI 1);
 by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
+by (blast_tac (!claset addIs [analz_increasing RS parts_mono RS subsetD]) 1);
 qed "parts_analz";
 Addsimps [parts_analz];
 
@@ -339,7 +339,7 @@
 goal thy "analz{} = {}";
 by (Step_tac 1);
 by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "analz_empty";
 Addsimps [analz_empty];
 
@@ -386,8 +386,7 @@
 by (etac analz.induct 1);
 by (Auto_tac());
 by (etac analz.induct 1);
-by (ALLGOALS
-    (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
+by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd]) 0));
 qed "analz_insert_MPair";
 
 (*Can pull out enCrypted message if the Key is not known*)
@@ -459,24 +458,24 @@
 
 goal thy "!!H. X: analz (analz H) ==> X: analz H";
 by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "analz_analzE";
-AddSEs [analz_analzE];
+AddSDs [analz_analzE];
 
 goal thy "analz (analz H) = analz H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "analz_idem";
 Addsimps [analz_idem];
 
 goal thy "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
 by (dtac analz_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "analz_trans";
 
 (*Cut; Lemma 2 of Lowe*)
 goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
 by (etac analz_trans 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "analz_cut";
 
 (*Cut can be proved easily by induction on
@@ -510,7 +509,7 @@
 \         analz H = H";
 by (Step_tac 1);
 by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "analz_trivial";
 
 (*Helps to prove Fake cases*)
@@ -544,7 +543,7 @@
 AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
 
 goal thy "H <= synth(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "synth_increasing";
 
 (*Monotonicity*)
@@ -569,39 +568,39 @@
 
 goal thy "!!H. X: synth (synth H) ==> X: synth H";
 by (etac synth.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "synth_synthE";
-AddSEs [synth_synthE];
+AddSDs [synth_synthE];
 
 goal thy "synth (synth H) = synth H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "synth_idem";
 
 goal thy "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
 by (dtac synth_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "synth_trans";
 
 (*Cut; Lemma 2 of Lowe*)
 goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
 by (etac synth_trans 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "synth_cut";
 
 goal thy "Agent A : synth H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Agent_synth";
 
 goal thy "(Nonce N : synth H) = (Nonce N : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Nonce_synth_eq";
 
 goal thy "(Key K : synth H) = (Key K : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Key_synth_eq";
 
 goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Crypt_synth_eq";
 
 Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
@@ -609,7 +608,7 @@
 
 goalw thy [keysFor_def]
     "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "keysFor_synth";
 Addsimps [keysFor_synth];
 
@@ -655,11 +654,10 @@
 by (best_tac
     (!claset addEs [impOfSubs synth_increasing,
                     impOfSubs analz_mono]) 5);
-by (Best_tac 1);
-by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
-by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
-by (deepen_tac (!claset addSEs [analz.Decrypt]
-                        addIs  [analz.Decrypt]) 0 1);
+by (Blast_tac 1);
+by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
+by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1);
+by (blast_tac (!claset addIs [analz.Decrypt]) 1);
 qed "analz_UN1_synth";
 Addsimps [analz_UN1_synth];
 
@@ -668,7 +666,7 @@
 
 goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
 by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "parts_insert_subset_Un";
 
 (*More specifically for Fake*)
@@ -676,7 +674,7 @@
 \              parts (insert X H) <= synth (analz G) Un parts G Un parts H";
 by (dtac parts_insert_subset_Un 1);
 by (Full_simp_tac 1);
-by (Deepen_tac 0 1);
+by (Blast_tac 1);
 qed "Fake_parts_insert";
 
 goal thy
@@ -696,15 +694,15 @@
 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
                       addSEs [impOfSubs analz_mono]) 2);
 by (Full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Fake_analz_insert";
 
 goal thy "(X: analz H & X: parts H) = (X: analz H)";
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
 val analz_conj_parts = result();
 
 goal thy "(X: analz H | X: parts H) = (X: parts H)";
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
 val analz_disj_parts = result();
 
 AddIffs [analz_conj_parts, analz_disj_parts];
@@ -713,20 +711,20 @@
   redundant cases*)
 goal thy "({|X,Y|} : synth (analz H)) = \
 \         (X : synth (analz H) & Y : synth (analz H))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "MPair_synth_analz";
 
 AddIffs [MPair_synth_analz];
 
 goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
 \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Crypt_synth_analz";
 
 
 goal thy "!!K. X ~: synth (analz H) \
 \   ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Hash_synth_analz";
 Addsimps [Hash_synth_analz];
 
@@ -798,7 +796,7 @@
 \   ==> (Hash[X] Y : synth (analz H)) = \
 \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "HPair_synth_analz";
 
 Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
@@ -866,6 +864,6 @@
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 goal Set.thy "A Un (B Un A) = B Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 val Un_absorb3 = result();
 Addsimps [Un_absorb3];
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -311,7 +311,7 @@
 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
@@ -327,7 +327,7 @@
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
 qed "Agent_not_see_encrypted_key";
 
 
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -125,12 +125,12 @@
 
 goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sees_Says_subset_insert";
 
 goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "sees_subset_sees_Says";
 
 (*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
@@ -141,7 +141,7 @@
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
     (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
-                       setloop split_tac [expand_if]))));
+				            setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
 goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
@@ -179,12 +179,12 @@
 \          (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
 by (list.induct_tac "evs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
+by (blast_tac (!claset addDs [impOfSubs initState_subset]) 1);
 by (rtac conjI 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (event.induct_tac "a" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed_spec_mp "seesD";
 
 Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
@@ -202,7 +202,7 @@
 
 goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
 by (etac (impOfSubs parts_mono) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usedI";
 
 AddIs [usedI];
@@ -222,7 +222,7 @@
 
 (*A session key cannot clash with a long-term shared key*)
 goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "shrK_neq";
 
 Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
@@ -264,7 +264,7 @@
 by (Step_tac 1);
 (*MPair case*)
 by (res_inst_tac [("x","Na+Nb")] exI 2);
-by (fast_tac (!claset addSEs [add_leE]) 2);
+by (blast_tac (!claset addSEs [add_leE]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
 by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
@@ -272,7 +272,7 @@
 
 goal thy "EX N. Nonce N ~: used evs";
 by (rtac (lemma RS exE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Nonce_supply1";
 
 goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
@@ -307,14 +307,14 @@
 goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
 by (rtac (lemma RS exE) 1);
 by (rtac selectI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Nonce_supply";
 
 (*** Supply fresh keys for possibility theorems. ***)
 
 goal thy "EX K. Key K ~: used evs";
 by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Key_supply1";
 
 val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
@@ -344,7 +344,7 @@
 goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
 by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
 by (rtac selectI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Key_supply";
 
 (*** Tactics for possibility theorems ***)
@@ -400,28 +400,23 @@
 val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
 
 goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_Compl_range";
 
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\         Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-qed "insert_Key_image";
-
 goal thy "insert (Key K) H = Key `` {K} Un H";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_Key_singleton";
 
 goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
-by (Fast_tac 1);
-qed "insert_Key_image'";
+by (Blast_tac 1);
+qed "insert_Key_image";
 
 val analz_image_freshK_ss = 
      !simpset delsimps [image_insert, image_Un]
               addsimps ([image_insert RS sym, image_Un RS sym,
                          Key_not_used, 
                          insert_Key_singleton, subset_Compl_range,
-                         insert_Key_image', Un_assoc RS sym]
+                         insert_Key_image, Un_assoc RS sym]
                         @disj_comms)
               setloop split_tac [expand_if];
 
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -27,8 +27,8 @@
 goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
 by (dB.induct_tac "s" 1);
 by (ALLGOALS(simp_tac (addsplit (!simpset))));
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "subst_not_free";
 Addsimps [subst_not_free RS eqTrueI];
 
@@ -36,7 +36,7 @@
 \                   (i < k & free t i | k < i & free t (pred i))";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
-by (fast_tac HOL_cs 2);
+by (Blast_tac 2);
 by(simp_tac (!simpset addsimps [pred_def]
                       setloop (split_tac [expand_nat_case])) 1);
 by (safe_tac HOL_cs);
@@ -48,7 +48,7 @@
 \              (free s k & free t i | free s (if i<k then i else Suc i))";
 by (dB.induct_tac "s" 1);
 by (Asm_simp_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (!simpset)) 2);
 by(simp_tac (!simpset addsimps [pred_def,subst_Var]
                       setloop (split_tac [expand_if,expand_nat_case])) 1);
@@ -94,17 +94,17 @@
 
 goal Eta.thy "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_Abs";
 
 goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppL";
 
 goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppR";
 
 goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
@@ -142,9 +142,9 @@
 goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
 by (dB.induct_tac "u" 1);
 by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
-by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
-by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
-by (fast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
+by (blast_tac (!claset addIs [r_into_rtrancl]) 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_App]) 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
 qed_spec_mp "rtrancl_eta_subst";
 
 goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
@@ -179,7 +179,7 @@
   by (etac thin_rl 1);
   by (res_inst_tac [("dB","t")] dB_case_distinction 1);
     by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-    by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
+    by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    by (Simp_tac 1);
   by (Simp_tac 1);
  by (Asm_simp_tac 1);
@@ -196,7 +196,7 @@
  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   by (Simp_tac 1);
-  by (fast_tac HOL_cs 1);
+  by (Blast_tac 1);
  by (Simp_tac 1);
 by (Asm_simp_tac 1);
 by (etac thin_rl 1);
@@ -211,7 +211,7 @@
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Blast_tac 1);
 qed_spec_mp "not_free_iff_lifted";
 
 goal Eta.thy "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -23,29 +23,30 @@
 
 goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_Abs";
 AddSIs [rtrancl_beta_Abs];
 
 goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppL";
 
 goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppR";
 
 goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
-by (deepen_tac (!claset addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
+by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
                         addIs  [rtrancl_trans]) 3 1);
 qed "rtrancl_beta_App";
 AddIs [rtrancl_beta_App];
 
 (*** subst and lift ***)
 
-fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]);
+fun addsplit ss = ss addsimps [subst_Var] 
+                     setloop  (split_inside_tac [expand_if]);
 
 goal Lambda.thy "(Var k)[u/k] = u";
 by (asm_full_simp_tac(addsplit(!simpset)) 1);
@@ -123,7 +124,7 @@
 goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
-by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
+by (blast_tac (!claset addDs [add_lessD1]) 1);
 qed "liftn_lift";
 Addsimps [liftn_lift];
 
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -21,7 +21,7 @@
 (*** beta <= par_beta <= beta^* ***)
 
 goal ParRed.thy "(Var n => t) = (t = Var n)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "par_beta_varL";
 Addsimps [par_beta_varL];
 
@@ -36,7 +36,7 @@
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac beta.induct 1);
-by (ALLGOALS(fast_tac (!claset addSIs [par_beta_refl])));
+by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl])));
 qed "beta_subset_par_beta";
 
 goal ParRed.thy "par_beta <= beta^*";
@@ -72,7 +72,7 @@
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac par_beta.induct 1);
-by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
+by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
 qed "diamond_par_beta";
 
 
@@ -83,16 +83,17 @@
   by (Simp_tac 1);
  by (etac rev_mp 1);
  by (dB.induct_tac "dB1" 1);
- by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
+ by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] 
+                                unsafe_addss (!simpset))));
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)
 
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (fast_tac (HOL_cs addIs [par_beta_cd]) 1);
+by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
 qed "diamond_par_beta2";
 
 goal ParRed.thy "confluent(beta)";
-by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
-                           par_beta_subset_beta,beta_subset_par_beta]) 1);
+by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
+			     par_beta_subset_beta, beta_subset_par_beta]) 1);
 qed"beta_confluent";
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/List.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -23,7 +23,6 @@
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
-by (REPEAT(resolve_tac [exI,refl,conjI] 1));
 qed "neq_Nil_conv";
 
 
@@ -31,10 +30,10 @@
 
 goal List.thy
  "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\                         (!y ys. xs=y#ys --> P(f y ys)))";
+\                        (!y ys. xs=y#ys --> P(f y ys)))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "expand_list_case";
 
 val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
@@ -44,8 +43,8 @@
 
 goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
 by (list.induct_tac "xs" 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 bind_thm("list_eq_cases",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
 
@@ -73,7 +72,7 @@
 goal List.thy "([] = xs@ys) = (xs=[] & ys=[])";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by(Blast_tac 1);
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
@@ -175,19 +174,19 @@
 goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "set_of_list_append";
 Addsimps[set_of_list_append];
 
 goal thy "(x mem xs) = (x: set_of_list xs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "set_of_list_mem_eq";
 
 goal List.thy "set_of_list l <= set_of_list (x#l)";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "set_of_list_subset_Cons";
 
 goal List.thy "(set_of_list xs = {}) = (xs = [])";
@@ -199,7 +198,7 @@
 goal List.thy "set_of_list(rev xs) = set_of_list(xs)";
 by(list.induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by(Blast_tac 1);
 qed "set_of_list_rev";
 Addsimps [set_of_list_rev];
 
@@ -227,7 +226,7 @@
 goal List.thy "list_all P xs = (!x. x mem xs --> P(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "list_all_mem_conv";
 
 
@@ -463,7 +462,7 @@
  by(ALLGOALS Asm_simp_tac);
 by(strip_tac 1);
 by(res_inst_tac [("n","n")] natE 1);
- by(Fast_tac 1);
+ by(Blast_tac 1);
 by(res_inst_tac [("n","i")] natE 1);
 by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
 qed_spec_mp "nth_take";
@@ -486,7 +485,7 @@
 by(list.induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Fast_tac 1);
+by(Blast_tac 1);
 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 Addsimps [takeWhile_append1];
 
@@ -503,7 +502,7 @@
 by(list.induct_tac "xs" 1);
  by(Simp_tac 1);
 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Fast_tac 1);
+by(Blast_tac 1);
 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 Addsimps [dropWhile_append1];
 
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -28,7 +28,7 @@
     "[| i: Nat;  P(Zero_Rep);   \
 \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "Nat_induct";
 
 val prems = goalw thy [Zero_def,Suc_def]
@@ -65,7 +65,7 @@
 by (fast_tac (!claset addSEs prems) 1);
 by (nat_ind_tac "n" 1);
 by (rtac (refl RS disjI1) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "natE";
 
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
@@ -126,17 +126,17 @@
 (*** nat_case -- the selection operator for nat ***)
 
 goalw thy [nat_case_def] "nat_case a f 0 = a";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "nat_case_0";
 
 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "nat_case_Suc";
 
 (** Introduction rules for 'pred_nat' **)
 
 goalw thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_natI";
 
 val major::prems = goalw thy [pred_nat_def]
@@ -149,8 +149,8 @@
 goalw thy [wf_def] "wf(pred_nat)";
 by (strip_tac 1);
 by (nat_ind_tac "x" 1);
-by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
-by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
+by (blast_tac (!claset addSEs [mp, pred_natE]) 2);
+by (blast_tac (!claset addSEs [mp, pred_natE]) 1);
 qed "wf_pred_nat";
 
 
@@ -228,7 +228,7 @@
 (** Elimination properties **)
 
 val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
-by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+by (blast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 qed "less_not_sym";
 
 (* [| n<m; m<n |] ==> R *)
@@ -243,7 +243,7 @@
 bind_thm ("less_irrefl", (less_not_refl RS notE));
 
 goal thy "!!m. n<m ==> m ~= (n::nat)";
-by (fast_tac (!claset addEs [less_irrefl]) 1);
+by (blast_tac (!claset addEs [less_irrefl]) 1);
 qed "less_not_refl2";
 
 
@@ -272,14 +272,13 @@
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
 by (rtac (major RS lessE) 1);
 by (rtac eq 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (rtac less 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "less_SucE";
 
 goal thy "(m < Suc(n)) = (m < n | m = n)";
-by (fast_tac (!claset addSIs [lessI]
-                      addEs  [less_trans, less_SucE]) 1);
+by (fast_tac (!claset addEs  [less_trans, less_SucE]) 1);
 qed "less_Suc_eq";
 
 val prems = goal thy "m<n ==> n ~= 0";
@@ -316,14 +315,13 @@
 qed "Suc_lessE";
 
 goal thy "!!m n. Suc(m) < Suc(n) ==> m<n";
-by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
+by (blast_tac (!claset addEs [lessE, make_elim Suc_lessD]) 1);
 qed "Suc_less_SucD";
 
 goal thy "!!m n. m<n ==> Suc(m) < Suc(n)";
 by (etac rev_mp 1);
 by (nat_ind_tac "n" 1);
-by (ALLGOALS (fast_tac (!claset addSIs [lessI]
-                                addEs  [less_trans, lessE])));
+by (ALLGOALS (fast_tac (!claset addEs  [less_trans, lessE])));
 qed "Suc_mono";
 
 
@@ -333,7 +331,7 @@
 Addsimps [Suc_less_eq];
 
 goal thy "~(Suc(n) < n)";
-by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
+by (blast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
 qed "not_Suc_n_less_n";
 Addsimps [not_Suc_n_less_n];
 
@@ -341,7 +339,7 @@
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (!simpset)));
 by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
 qed_spec_mp "less_trans_Suc";
 
 (*"Less than" is a linear ordering*)
@@ -350,7 +348,7 @@
 by (nat_ind_tac "n" 1);
 by (rtac (refl RS disjI1 RS disjI2) 1);
 by (rtac (zero_less_Suc RS disjI1) 1);
-by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
+by (fast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
 qed "less_linear";
 
 qed_goal "nat_less_cases" thy 
@@ -453,16 +451,16 @@
 val leE = make_elim leD;
 
 goal thy "(~n<m) = (m<=(n::nat))";
-by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
+by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
 qed "not_less_iff_le";
 
 goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "not_leE";
 
 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 qed "lessD";
 
 goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
@@ -474,32 +472,32 @@
         "!!m. Suc m <= n ==> m < n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (cut_facts_tac [less_linear] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Suc_le_lessD";
 
 goal thy "(Suc m <= n) = (m < n)";
-by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
+by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
 qed "Suc_le_eq";
 
 goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
 qed "le_SucI";
 Addsimps[le_SucI];
 
 bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
 
 goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)";
-by (fast_tac (!claset addEs [less_asym]) 1);
+by (blast_tac (!claset addEs [less_asym]) 1);
 qed "less_imp_le";
 
 goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 qed "le_imp_less_or_eq";
 
 goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 by (flexflex_tac);
 qed "less_or_eq_imp_le";
 
@@ -522,13 +520,16 @@
 qed "less_le_trans";
 
 goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
-          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
+by (EVERY1[dtac le_imp_less_or_eq, 
+	   dtac le_imp_less_or_eq,
+	   rtac less_or_eq_imp_le, 
+	   fast_tac (!claset addIs [less_trans])]);
 qed "le_trans";
 
-val prems = goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
-          fast_tac (!claset addEs [less_irrefl,less_asym])]);
+goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
+by (EVERY1[dtac le_imp_less_or_eq, 
+	   dtac le_imp_less_or_eq,
+	   blast_tac (!claset addEs [less_irrefl,less_asym])]);
 qed "le_anti_sym";
 
 goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
@@ -543,7 +544,7 @@
  br conjI 1;
   be less_imp_le 1;
  be (less_not_refl2 RS not_sym) 1;
-by(fast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
+by(blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
 qed "nat_less_le";
 
 (** LEAST -- the least number operator **)
@@ -551,9 +552,9 @@
 val [prem1,prem2] = goalw thy [Least_def]
     "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
 by (rtac select_equality 1);
-by (fast_tac (!claset addSIs [prem1,prem2]) 1);
+by (blast_tac (!claset addSIs [prem1,prem2]) 1);
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
+by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
 qed "Least_equality";
 
 val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
@@ -564,7 +565,7 @@
 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
 by (assume_tac 1);
 by (assume_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
@@ -576,7 +577,7 @@
 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
 by (assume_tac 1);
 by (rtac le_refl 2);
-by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
+by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1);
 qed "Least_le";
 
 val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
@@ -593,23 +594,23 @@
         safe_tac (!claset addSEs [LeastI]),
         rename_tac "j" 1,
         res_inst_tac [("n","j")] natE 1,
-        Fast_tac 1,
-        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
+        Blast_tac 1,
+        blast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
         rename_tac "k n" 1,
         res_inst_tac [("n","k")] natE 1,
-        Fast_tac 1,
+        Blast_tac 1,
         hyp_subst_tac 1,
         rewtac Least_def,
         rtac (select_equality RS arg_cong RS sym) 1,
         safe_tac (!claset),
         dtac Suc_mono 1,
-        Fast_tac 1,
+        Blast_tac 1,
         cut_facts_tac [less_linear] 1,
         safe_tac (!claset),
         atac 2,
-        Fast_tac 2,
+        Blast_tac 2,
         dtac Suc_mono 1,
-        Fast_tac 1]);
+        Blast_tac 1]);
 
 
 (*** Instantiation of transitivity prover ***)
@@ -633,8 +634,8 @@
   (fn _ => [etac swap2 1, etac leD 1]);
 val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
   (fn _ => [etac less_SucE 1,
-            fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
-                             addDs [less_trans_Suc]) 1,
+            fast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
+                              addDs [less_trans_Suc]) 1,
             atac 1]);
 val leD = le_eq_less_Suc RS iffD1;
 val not_lessD = nat_leI RS leD;
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Relation.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -9,7 +9,7 @@
 (** Identity relation **)
 
 goalw Relation.thy [id_def] "(a,a) : id";  
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "idI";
 
 val major::prems = goalw Relation.thy [id_def]
@@ -21,7 +21,7 @@
 qed "idE";
 
 goalw Relation.thy [id_def] "(a,b):id = (a=b)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pair_in_id_conv";
 Addsimps [pair_in_id_conv];
 
@@ -30,7 +30,7 @@
 
 goalw Relation.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";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -55,12 +55,12 @@
 AddSEs [compE, idE];
 
 goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_mono";
 
 goal Relation.thy
     "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "comp_subset_Sigma";
 
 (** Natural deduction for trans(r) **)
@@ -72,7 +72,7 @@
 
 goalw Relation.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";
 
 (** Natural deduction for converse(r) **)
@@ -88,7 +88,7 @@
 qed "converseI";
 
 goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "converseD";
 
 (*More general than converseD, as it "splits" the member of the relation*)
@@ -104,14 +104,14 @@
 AddSEs [converseE];
 
 goalw Relation.thy [converse_def] "converse(converse R) = R";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "converse_converse";
 
 (** Domain **)
 
 qed_goalw "Domain_iff" Relation.thy [Domain_def]
     "a: Domain(r) = (EX y. (a,y): r)"
- (fn _=> [ (Fast_tac 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
 
 qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
  (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
@@ -144,16 +144,16 @@
 
 qed_goalw "Image_iff" Relation.thy [Image_def]
     "b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
 qed_goal "Image_singleton_iff" Relation.thy
     "(b : r^^{a}) = ((a,b):r)"
  (fn _ => [ rtac (Image_iff RS trans) 1,
-            Fast_tac 1 ]);
+            Blast_tac 1 ]);
 
 qed_goalw "ImageI" Relation.thy [Image_def]
     "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
- (fn _ => [ (Fast_tac 1)]);
+ (fn _ => [ (Blast_tac 1)]);
 
 qed_goalw "ImageE" Relation.thy [Image_def]
     "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Set.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -151,10 +151,10 @@
 AddEs  [subsetD, subsetCE];
 
 qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
- (fn _=> [Fast_tac 1]);
+ (fn _=> [Blast_tac 1]);
 
 val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_trans";
 
 
@@ -206,7 +206,7 @@
 section "The empty set -- {}";
 
 qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [empty_iff];
 
@@ -216,14 +216,14 @@
 AddSEs [emptyE];
 
 qed_goal "empty_subsetI" Set.thy "{} <= A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
  (fn [prem]=>
   [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
 
 qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 goal Set.thy "Ball {} P = True";
 by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
@@ -235,13 +235,13 @@
 Addsimps [ball_empty, bex_empty];
 
 goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
-by(Fast_tac 1);
+by(Blast_tac 1);
 qed "ball_False";
 Addsimps [ball_False];
 
 (* The dual is probably not helpful:
 goal Set.thy "(? x:A.True) = (A ~= {})";
-by(Fast_tac 1);
+by(Blast_tac 1);
 qed "bex_True";
 Addsimps [bex_True];
 *)
@@ -267,7 +267,7 @@
 section "Set complement -- Compl";
 
 qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Compl_iff];
 
@@ -293,7 +293,7 @@
 section "Binary union -- Un";
 
 qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Un_iff];
 
@@ -324,7 +324,7 @@
 section "Binary intersection -- Int";
 
 qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Int_iff];
 
@@ -353,7 +353,7 @@
 section "Set difference";
 
 qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Diff_iff];
 
@@ -378,7 +378,7 @@
 section "Augmenting a set -- insert";
 
 qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
 
 Addsimps [insert_iff];
 
@@ -409,13 +409,13 @@
  (fn _=> [ (rtac insertI1 1) ]);
 
 goal Set.thy "!!a. b : {a} ==> b=a";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "singletonD";
 
 bind_thm ("singletonE", make_elim singletonD);
 
 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
-(fn _ => [Fast_tac 1]);
+(fn _ => [Blast_tac 1]);
 
 goal Set.thy "!!a b. {a}={b} ==> a=b";
 by (fast_tac (!claset addEs [equalityE]) 1);
@@ -439,7 +439,7 @@
 section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
 
 goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_iff";
 
 Addsimps [UN_iff];
@@ -507,7 +507,7 @@
 
 goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN1_iff";
 
 Addsimps [UN1_iff];
@@ -531,7 +531,7 @@
 
 goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT1_iff";
 
 Addsimps [INT1_iff];
@@ -552,7 +552,7 @@
 section "Union";
 
 goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_iff";
 
 Addsimps [Union_iff];
@@ -575,7 +575,7 @@
 section "Inter";
 
 goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_iff";
 
 Addsimps [Inter_iff];
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Sum.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -53,12 +53,12 @@
 
 val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inl_Rep_inject";
 
 val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inr_Rep_inject";
 
 goalw Sum.thy [Inl_def] "inj(Inl)";
@@ -78,11 +78,11 @@
 val Inr_inject = inj_Inr RS injD;
 
 goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-by (fast_tac (!claset addSEs [Inl_inject]) 1);
+by (blast_tac (!claset addSDs [Inl_inject]) 1);
 qed "Inl_eq";
 
 goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-by (fast_tac (!claset addSEs [Inr_inject]) 1);
+by (blast_tac (!claset addSDs [Inr_inject]) 1);
 qed "Inr_eq";
 
 AddIffs [Inl_eq, Inr_eq];
@@ -92,11 +92,11 @@
 (** Introduction rules for the injections **)
 
 goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InlI";
 
 goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "InrI";
 
 (** Elimination rules **)
@@ -119,7 +119,7 @@
 (** sum_case -- the selection operator for sums **)
 
 goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "sum_case_Inl";
 
 goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
@@ -163,7 +163,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);
@@ -177,12 +177,15 @@
 by (REPEAT (ares_tac prems 1));
 qed "PartE";
 
+AddIs  [Part_eqI];
+AddSEs [PartE];
+
 goalw Sum.thy [Part_def] "Part A h <= A";
 by (rtac Int_lower1 1);
 qed "Part_subset";
 
 goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
+by (Fast_tac 1);
 qed "Part_mono";
 
 val basic_monos = basic_monos @ [Part_mono];
@@ -192,14 +195,14 @@
 qed "PartD1";
 
 goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Blast_tac 1);
 qed "Part_id";
 
 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Fast_tac 1);
 qed "Part_Int";
 
 (*For inductive definitions*)
 goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Fast_tac 1);
 qed "Part_Collect";
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Trancl.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -20,7 +20,7 @@
 (*Reflexivity of rtrancl*)
 goal Trancl.thy "(a,a) : r^*";
 by (stac rtrancl_unfold 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rtrancl_refl";
 
 Addsimps [rtrancl_refl];
@@ -30,7 +30,7 @@
 (*Closure under composition with r*)
 goal Trancl.thy "!!r. [| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
 by (stac rtrancl_unfold 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rtrancl_into_rtrancl";
 
 (*rtrancl of r contains r*)
@@ -64,7 +64,7 @@
 (*by induction on this formula*)
 by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
 (*now solve first subgoal: this formula is sufficient*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 (*now do the induction*)
 by (resolve_tac [major RS rtrancl_full_induct] 1);
 by (fast_tac (!claset addIs prems) 1);
@@ -124,7 +124,7 @@
 by (dtac rtrancl_mono 1);
 by (dtac rtrancl_mono 1);
 by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rtrancl_subset";
 
 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
@@ -165,7 +165,7 @@
 \     ==> P(a)";
 by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
 by (resolve_tac prems 1);
-by (fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
+by (fast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
 qed "converse_rtrancl_induct";
 
 val prems = goal Trancl.thy
@@ -225,7 +225,7 @@
 (*by induction on this formula*)
 by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
 (*now solve first subgoal: this formula is sufficient*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (etac rtrancl_induct 1);
 by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
 qed "trancl_induct";
@@ -240,7 +240,7 @@
 by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
 by (etac rtranclE 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
 qed "tranclE";
 
@@ -268,11 +268,11 @@
 by (cut_facts_tac prems 1);
 by (rtac (major RS rtrancl_induct) 1);
 by (rtac (refl RS disjI1) 1);
-by (fast_tac (!claset addSEs [SigmaE2]) 1);
+by (Blast_tac 1);
 val lemma = result();
 
 goalw Trancl.thy [trancl_def]
     "!!r. r <= A Times A ==> r^+ <= A Times A";
-by (fast_tac (!claset addSDs [lemma]) 1);
+by (blast_tac (!claset addSDs [lemma]) 1);
 qed "trancl_subset_Sigma";
 
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Univ.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -69,12 +69,12 @@
 (*** Introduction rules for Node ***)
 
 goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Node_K0_I";
 
 goalw Univ.thy [Node_def,Push_def]
     "!!p. p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
 qed "Node_Push_I";
 
 
@@ -98,12 +98,12 @@
 (** Atomic nodes **)
 
 goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
-by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
+by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;
 
 goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (!claset addSEs [Atom_inject]) 1);
+by (blast_tac (!claset addSDs [Atom_inject]) 1);
 qed "Atom_Atom_eq";
 AddIffs [Atom_Atom_eq];
 
@@ -142,14 +142,12 @@
 
 (** Injectiveness of Scons **)
 
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma1";
 
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
+by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
@@ -171,7 +169,7 @@
 AddSDs [Scons_inject];
 
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
-by (fast_tac (!claset addSEs [Scons_inject]) 1);
+by (blast_tac (!claset addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";
 
 (*** Distinctness involving Leaf and Numb ***)
@@ -244,7 +242,7 @@
 (*** ntrunc applied to the various node sets ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_0";
 
 goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
@@ -261,7 +259,7 @@
 
 goalw Univ.thy [Scons_def,ntrunc_def]
     "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
-by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
+by (safe_tac (!claset addSIs [equalityI, imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
             rtac (ndepth_Push_Node RS subst) 1 THEN 
@@ -273,7 +271,7 @@
 goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_one_In0";
 
 goalw Univ.thy [In0_def]
@@ -284,7 +282,7 @@
 goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_one_In1";
 
 goalw Univ.thy [In1_def]
@@ -321,11 +319,11 @@
 (*** Disjoint Sum ***)
 
 goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_In0I";
 
 goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_In1I";
 
 val major::prems = goalw Univ.thy [usum_def]
@@ -363,12 +361,12 @@
 (*** proving equality of sets and functions using ntrunc ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_subsetI";
 
 val [major] = goalw Univ.thy [ntrunc_def]
     "(!!k. ntrunc k M <= N) ==> M<=N";
-by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
+by (blast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
                             major RS subsetD]) 1);
 qed "ntrunc_subsetD";
 
@@ -390,15 +388,15 @@
 (*** Monotonicity ***)
 
 goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "uprod_mono";
 
 goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_mono";
 
 goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_mono";
 
 goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
@@ -413,29 +411,29 @@
 (*** Split and Case ***)
 
 goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Split";
 
 goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In0";
 
 goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In1";
 
 (**** UN x. B(x) rules ****)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_UN1";
 
 goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_UN1_x";
 
 goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_UN1_y";
 
 goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
@@ -450,7 +448,7 @@
 (*** Equality : the diagonal relation ***)
 
 goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "diag_eqI";
 
 val diagI = refl RS diag_eqI |> standard;
@@ -468,7 +466,7 @@
 
 goalw Univ.thy [dprod_def]
     "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprodI";
 
 (*The general elimination rule*)
@@ -485,11 +483,11 @@
 (*** Equality for Disjoint Sum ***)
 
 goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_In0I";
 
 goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_In1I";
 
 val major::prems = goalw Univ.thy [dsum_def]
@@ -510,22 +508,22 @@
 (*** Monotonicity ***)
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_mono";
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_mono";
 
 
 (*** Bounding theorems ***)
 
 goal Univ.thy "diag(A) <= A Times A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "diag_subset_Sigma";
 
 goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_Sigma";
 
 val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
@@ -535,11 +533,11 @@
     "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
 by (safe_tac (!claset));
 by (stac Split 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_subset_Sigma2";
 
 goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_Sigma";
 
 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
@@ -548,15 +546,15 @@
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_dsum";
 
 Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/equalities.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -13,12 +13,12 @@
 section "{}";
 
 goal Set.thy "{x.False} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Collect_False_empty";
 Addsimps [Collect_False_empty];
 
 goal Set.thy "(A <= {}) = (A = {})";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_empty";
 Addsimps [subset_empty];
 
@@ -26,7 +26,7 @@
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
 goal Set.thy "insert a A = {a} Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_is_Un";
 
 goal Set.thy "insert a A ~= {}";
@@ -38,55 +38,55 @@
 Addsimps[empty_not_insert];
 
 goal Set.thy "!!a. a:A ==> insert a A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_absorb";
 
 goal Set.thy "insert x (insert x A) = insert x A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_absorb2";
 Addsimps [insert_absorb2];
 
 goal Set.thy "insert x (insert y A) = insert y (insert x A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_commute";
 
 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_subset";
 Addsimps[insert_subset];
 
 (* use new B rather than (A-{a}) to avoid infinite unfolding *)
 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
 by (res_inst_tac [("x","A-{a}")] exI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "mk_disjoint_insert";
 
 goal Set.thy
     "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_insert_distrib";
 
 goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN1_insert_distrib";
 
 section "``";
 
 goal Set.thy "f``{} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_empty";
 Addsimps[image_empty];
 
 goal Set.thy "f``insert a B = insert (f a) (f``B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_insert";
 Addsimps[image_insert];
 
 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
 
 goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
 
@@ -94,7 +94,7 @@
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
 by (split_tac [expand_if] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "if_image_distrib";
 Addsimps[if_image_distrib];
 
@@ -102,53 +102,53 @@
 section "range";
 
 qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
 
 qed_goalw "image_range" Set.thy [image_def]
  "f``range g = range (%x. f (g x))" 
- (fn _ => [rtac Collect_cong 1, Fast_tac 1]);
+ (fn _ => [rtac Collect_cong 1, Blast_tac 1]);
 
 section "Int";
 
 goal Set.thy "A Int A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_absorb";
 Addsimps[Int_absorb];
 
 goal Set.thy "A Int B  =  B Int A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_commute";
 
 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_assoc";
 
 goal Set.thy "{} Int B = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_empty_left";
 Addsimps[Int_empty_left];
 
 goal Set.thy "A Int {} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_empty_right";
 Addsimps[Int_empty_right];
 
 goal Set.thy "UNIV Int B = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_UNIV_left";
 Addsimps[Int_UNIV_left];
 
 goal Set.thy "A Int UNIV = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_UNIV_right";
 Addsimps[Int_UNIV_right];
 
 goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_Un_distrib";
 
 goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_Un_distrib2";
 
 goal Set.thy "(A<=B) = (A Int B = A)";
@@ -163,53 +163,53 @@
 section "Un";
 
 goal Set.thy "A Un A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_absorb";
 Addsimps[Un_absorb];
 
 goal Set.thy "A Un B  =  B Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_commute";
 
 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_assoc";
 
 goal Set.thy "{} Un B = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_empty_left";
 Addsimps[Un_empty_left];
 
 goal Set.thy "A Un {} = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_empty_right";
 Addsimps[Un_empty_right];
 
 goal Set.thy "UNIV Un B = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_UNIV_left";
 Addsimps[Un_UNIV_left];
 
 goal Set.thy "A Un UNIV = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_UNIV_right";
 Addsimps[Un_UNIV_right];
 
 goal Set.thy "(insert a B) Un C = insert a (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_insert_left";
 
 goal Set.thy "A Un (insert a B) = insert a (A Un B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_insert_right";
 
 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_Int_distrib";
 
 goal Set.thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_Int_crazy";
 
 goal Set.thy "(A<=B) = (A Un B = B)";
@@ -217,7 +217,7 @@
 qed "subset_Un_eq";
 
 goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_insert_iff";
 
 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
@@ -228,33 +228,33 @@
 section "Compl";
 
 goal Set.thy "A Int Compl(A) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_disjoint";
 Addsimps[Compl_disjoint];
 
 goal Set.thy "A Un Compl(A) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_partition";
 
 goal Set.thy "Compl(Compl(A)) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "double_complement";
 Addsimps[double_complement];
 
 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_Un";
 
 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_Int";
 
 goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_UN";
 
 goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_INT";
 
 (*Halmos, Naive Set Theory, page 16.*)
@@ -267,27 +267,27 @@
 section "Union";
 
 goal Set.thy "Union({}) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_empty";
 Addsimps[Union_empty];
 
 goal Set.thy "Union(UNIV) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_UNIV";
 Addsimps[Union_UNIV];
 
 goal Set.thy "Union(insert a B) = a Un Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_insert";
 Addsimps[Union_insert];
 
 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_Un_distrib";
 Addsimps[Union_Un_distrib];
 
 goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_Int_subset";
 
 val prems = goal Set.thy
@@ -298,26 +298,26 @@
 section "Inter";
 
 goal Set.thy "Inter({}) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_empty";
 Addsimps[Inter_empty];
 
 goal Set.thy "Inter(UNIV) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_UNIV";
 Addsimps[Inter_UNIV];
 
 goal Set.thy "Inter(insert a B) = a Int Inter(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_insert";
 Addsimps[Inter_insert];
 
 goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_Un_subset";
 
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
 qed "Inter_Un_distrib";
 
 section "UN and INT";
@@ -325,134 +325,134 @@
 (*Basic identities*)
 
 goal Set.thy "(UN x:{}. B x) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_empty";
 Addsimps[UN_empty];
 
 goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_UNIV";
 Addsimps[UN_UNIV];
 
 goal Set.thy "(INT x:{}. B x) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_empty";
 Addsimps[INT_empty];
 
 goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_UNIV";
 Addsimps[INT_UNIV];
 
 goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_insert";
 Addsimps[UN_insert];
 
 goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_insert";
 Addsimps[INT_insert];
 
 goal Set.thy
     "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_insert_distrib";
 
 goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT1_insert_distrib";
 
 goal Set.thy "Union(range(f)) = (UN x.f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_range_eq";
 
 goal Set.thy "Inter(range(f)) = (INT x.f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_range_eq";
 
 goal Set.thy "Union(B``A) = (UN x:A. B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_image_eq";
 
 goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_image_eq";
 
 goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_constant";
 
 goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_constant";
 
 goal Set.thy "(UN x.B) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN1_constant";
 Addsimps[UN1_constant];
 
 goal Set.thy "(INT x.B) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT1_constant";
 Addsimps[INT1_constant];
 
 goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_eq";
 
 (*Look: it has an EXISTENTIAL quantifier*)
 goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_eq";
 
 (*Distributive laws...*)
 
 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_Union";
 
 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
    Union of a family of unions **)
 goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_Union_image";
 
 (*Equivalent version*)
 goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_Un_distrib";
 
 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_Inter";
 
 goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
 qed "Int_Inter_image";
 
 (*Equivalent version*)
 goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "INT_Int_distrib";
 
 (*Halmos, Naive Set Theory, page 35.*)
 goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_UN_distrib";
 
 goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_INT_distrib";
 
 goal Set.thy
     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_UN_distrib2";
 
 goal Set.thy
     "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_INT_distrib2";
 
 
@@ -462,58 +462,58 @@
     body and (b) there are no similar rules for Int. **)
 
 goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ball_Un";
 
 goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "bex_Un";
 
 
 section "-";
 
 goal Set.thy "A-A = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_cancel";
 Addsimps[Diff_cancel];
 
 goal Set.thy "{}-A = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "empty_Diff";
 Addsimps[empty_Diff];
 
 goal Set.thy "A-{} = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_empty";
 Addsimps[Diff_empty];
 
 goal Set.thy "A-UNIV = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_UNIV";
 Addsimps[Diff_UNIV];
 
 goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_insert0";
 Addsimps [Diff_insert0];
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
 goal Set.thy "A - insert a B = A - B - {a}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
 goal Set.thy "A - insert a B = A - {a} - B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_insert2";
 
 goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
 by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_Diff_if";
 
 goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_Diff1";
 Addsimps [insert_Diff1];
 
@@ -522,24 +522,24 @@
 qed "insert_Diff";
 
 goal Set.thy "A Int (B-A) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_disjoint";
 Addsimps[Diff_disjoint];
 
 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_partition";
 
 goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "double_diff";
 
 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_Un";
 
 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_Int";
 
 Addsimps[subset_UNIV, empty_subsetI, subset_refl];
@@ -547,7 +547,7 @@
 
 (** Miniscoping: pushing in big Unions and Intersections **)
 local
-  fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1])
+  fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1])
 in
 val UN1_simps = map prover 
                 ["(UN x. insert a (B x)) = insert a (UN x. B x)",
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/ex/Mutil.ML
--- a/src/HOL/ex/Mutil.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/ex/Mutil.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -16,8 +16,8 @@
 \              u: tiling A --> t <= Compl u --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addIs tiling.intrs
-                      addss (!simpset addsimps [Un_assoc])) 1);
+by (simp_tac (!simpset addsimps [Un_assoc]) 1);
+by (blast_tac (!claset addIs tiling.intrs) 1);
 qed_spec_mp "tiling_UnI";
 
 
@@ -29,19 +29,19 @@
 goal thy "ALL i. (i: below k) = (i<k)";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "below_less_iff";
 
 Addsimps [below_less_iff];
 
 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Sigma_Suc1";
 
 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Sigma_Suc2";
 
 (*Deletion is essential to allow use of Sigma_Suc1,2*)
@@ -55,17 +55,17 @@
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
 \    {(i, n1+n1), (i, Suc(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  [less_asym]
-                      addSDs [below_less_iff RS iffD1]) 1);
+by (blast_tac (!claset addEs  [less_irrefl, less_asym]
+                       addSDs [below_less_iff RS iffD1]) 1);
 qed "dominoes_tile_row";
 
 goal thy "(below m) Times below(n + n) : tiling domino";
 by (nat_ind_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row] 
-                      addEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
+by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
+                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
 qed "dominoes_tile_matrix";
 
 
@@ -83,11 +83,11 @@
 bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
 
 goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "evnodd_Un";
 
 goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "evnodd_Diff";
 
 goalw thy [evnodd_def] "evnodd {} b = {}";
@@ -113,12 +113,12 @@
 by (REPEAT (asm_full_simp_tac (!simpset addsimps
                           [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
                           setloop split_tac [expand_if]) 1
-           THEN Fast_tac 1));
+           THEN Blast_tac 1));
 qed "domino_singleton";
 
 goal thy "!!d. d:domino ==> finite d";
-by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
-                      addEs [domino.elim]) 1);
+by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
+                      addSEs [domino.elim]) 1);
 qed "domino_finite";
 
 
@@ -127,7 +127,7 @@
 goal thy "!!t. t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
 by (rtac finite_emptyI 1);
-by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1);
+by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
 qed "tiling_domino_finite";
 
 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
@@ -143,7 +143,7 @@
                                      tiling_domino_finite,
                                      evnodd_subset RS finite_subset,
                                      card_insert_disjoint]) 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 "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
diff -r f27002fc531d -r d8f254ad1ab9 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/ex/cla.ML	Fri Apr 04 11:18:52 1997 +0200
@@ -13,17 +13,17 @@
 set_current_thy "HOL";  (*Boosts efficiency by omitting redundant rules*)
 
 goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*If and only if*)
 
 goal HOL.thy "(P=Q) = (Q=P::bool)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 goal HOL.thy "~ (P = (~P))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 
@@ -40,112 +40,112 @@
 writeln"Pelletier's examples";
 (*1*)
 goal HOL.thy "(P-->Q)  =  (~Q --> ~P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*2*)
 goal HOL.thy "(~ ~ P) =  P";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*3*)
 goal HOL.thy "~(P-->Q) --> (Q-->P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*4*)
 goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*5*)
 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*6*)
 goal HOL.thy "P | ~ P";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*7*)
 goal HOL.thy "P | ~ ~ ~ P";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*8.  Peirce's law*)
 goal HOL.thy "((P-->Q) --> P)  -->  P";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*9*)
 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*10*)
 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
 goal HOL.thy "P=P::bool";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*12.  "Dijkstra's law"*)
 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*13.  Distributive law*)
 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*14*)
 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*15*)
 goal HOL.thy "(P --> Q) = (~P | Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*16*)
 goal HOL.thy "(P-->Q) | (Q-->P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*17*)
 goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Classical Logic: examples with quantifiers";
 
 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result(); 
 
 goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result(); 
 
 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result(); 
 
 goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result(); 
 
 (*From Wishnu Prasetya*)
 goal HOL.thy
    "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
 \   --> p(t) | r(t)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result(); 
 
 
@@ -153,60 +153,60 @@
 
 (*Needs multiple instantiation of the quantifier.*)
 goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 (*Needs double instantiation of the quantifier*)
 goal HOL.thy "? x. P(x) --> P(a) & P(b)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 goal HOL.thy "? z. P(z) --> (! x. P(x))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 goal HOL.thy "? x. (? y. P(y)) --> P(x)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";
 goal HOL.thy "? y. ! x. P(y)-->P(x)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result(); 
 
 writeln"Problem 19";
 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 20";
 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
 \   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
-by (Fast_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 21";
 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (Deepen_tac 1 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 22";
 goal HOL.thy "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
-by (Fast_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 23";
 goal HOL.thy "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
-by (Best_tac 1);  
+by (Blast_tac 1);  
 result();
 
 writeln"Problem 24";
 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
 \    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
 \   --> (? x. P(x)&R(x))";
-by (Fast_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 25";
@@ -215,14 +215,14 @@
 \       (! x. P(x) --> (M(x) & L(x))) &   \
 \       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
 \   --> (? x. Q(x)&P(x))";
-by (Best_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 26";
 goal HOL.thy "((? x. p(x)) = (? x. q(x))) &     \
 \     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 27";
@@ -231,7 +231,7 @@
 \             (! x. M(x) & L(x) --> P(x)) &   \
 \             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
 \         --> (! x. M(x) --> ~L(x))";
-by (Fast_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 28.  AMENDED";
@@ -239,21 +239,21 @@
 \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
 \       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
 \   --> (! x. P(x) & L(x) --> M(x))";
-by (Fast_tac 1);  
+by (Blast_tac 1);  
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
 goal HOL.thy "(? x. F(x)) & (? y. G(y))  \
 \   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
 \         (! x y. F(x) & G(y) --> H(x) & J(y)))";
-by (Fast_tac 1); 
+by (Blast_tac 1); 
 result();
 
 writeln"Problem 30";
 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
 \       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
 \   --> (! x. S(x))";
-by (Fast_tac 1);  
+by (Blast_tac 1);  
 result();
 
 writeln"Problem 31";
@@ -261,7 +261,7 @@
 \       (? x. L(x) & P(x)) & \
 \       (! x. ~ R(x) --> M(x))  \
 \   --> (? x. L(x) & M(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 32";
@@ -269,13 +269,13 @@
 \       (! x. S(x) & R(x) --> L(x)) & \
 \       (! x. M(x) --> R(x))  \
 \   --> (! x. P(x) & M(x) --> L(x))";
-by (Best_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 33";
 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
 \    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (Best_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 34  AMENDED (TWICE!!)";
@@ -284,13 +284,13 @@
 \                   ((? x. q(x)) = (! y. p(y))))   =    \
 \                  ((? x. ! y. q(x) = q(y))  =          \
 \                   ((? x. p(x)) = (! y. q(y))))";
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
 (*slower with smaller bounds*)
 result();
 
 writeln"Problem 35";
 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 36";
@@ -299,7 +299,7 @@
 \       (! x y. J x y | G x y -->       \
 \       (! z. J y z | G y z --> H x z))   \
 \   --> (! x. ? y. H x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 37";
@@ -308,7 +308,7 @@
 \       (! x z. ~(P x z) --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
 \   --> (! x. ? y. R x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 38";
@@ -318,35 +318,36 @@
 \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
 \          (~p(a) | ~(? y. p(y) & r x y) |                      \
 \           (? z. ? w. p(z) & r x w & r w z)))";
-by (Deepen_tac 0 1);  (*beats fast_tac!*)
+by (Blast_tac 1);  (*beats fast_tac!*)
 result();
 
 writeln"Problem 39";
 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 40.  AMENDED";
 goal HOL.thy "(? y. ! x. F x y = F x x)  \
 \       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 41";
 goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
 \              --> ~ (? z. ! x. f x z)";
-by (Best_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 42";
 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
 result();
 
-writeln"Problem 43  NOT PROVED AUTOMATICALLY";
+writeln"Problem 43!!";
 goal HOL.thy
     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
 \ --> (! x. (! y. q x y = (q y x::bool)))";
+by (Blast_tac 1);
 
 
 writeln"Problem 44";
@@ -354,7 +355,7 @@
 \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
 \             (? x. j(x) & (! y. g(y) --> h x y))               \
 \             --> (? x. j(x) & ~f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 45";
@@ -365,7 +366,7 @@
 \    (? x. f(x) & (! y. h x y --> l(y))                         \
 \               & (! y. g(y) & h x y --> j x y))                \
 \     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
-by (Best_tac 1); 
+by (Blast_tac 1); 
 result();
 
 
@@ -373,7 +374,7 @@
 
 writeln"Problem 48";
 goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 49  NOT PROVED AUTOMATICALLY";
@@ -386,20 +387,20 @@
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
 by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 51";
 goal HOL.thy
     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
 \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
-by (Best_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 52";
@@ -407,7 +408,7 @@
 goal HOL.thy
     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
 \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
-by (Best_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 55";
@@ -423,20 +424,20 @@
 \  (!x. hates agatha x --> hates butler x) & \
 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
 \   killed ?who agatha";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 56";
 goal HOL.thy
     "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 57";
 goal HOL.thy
     "P (f a b) (f b c) & P (f b c) (f a c) & \
 \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
@@ -447,13 +448,13 @@
 
 writeln"Problem 59";
 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 60";
 goal HOL.thy
     "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
@@ -461,7 +462,7 @@
     "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
 \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
 \            (~ p a | ~ p(f x) | p(f(f x))))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
@@ -470,14 +471,14 @@
     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();
 
 goal Prod.thy
     "(ALL x y. R(x,y) | R(y,x)) &                \
 \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
 \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 result();