# HG changeset patch
# User paulson
# Date 860764896 -7200
# Node ID 998cb95fdd43d10103ce80ee0ceffaa4e57c6b70
# Parent  bd922fc9001bc769e4e51a0edca56a8cb46683ff
Yet more fast_tac->blast_tac, and other tidying

diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Fun.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -23,7 +23,7 @@
 
 val prems = goalw Fun.thy [inj_def]
     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "injI";
 
 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
@@ -69,7 +69,7 @@
 
 val prems = goalw Fun.thy [inj_onto_def]
     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "inj_ontoI";
 
 val [major] = goal Fun.thy 
@@ -86,7 +86,7 @@
 qed "inj_ontoD";
 
 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
-by (fast_tac (!claset addSEs [inj_ontoD]) 1);
+by (blast_tac (!claset addSDs [inj_ontoD]) 1);
 qed "inj_onto_iff";
 
 val major::prems = goal Fun.thy
@@ -105,7 +105,7 @@
 qed "comp_inj";
 
 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
-by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
+by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
 qed "inj_imp";
 
 val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
@@ -118,9 +118,7 @@
 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
 qed "inv_injective";
 
-val prems = goal Fun.thy
-    "[| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
-by (cut_facts_tac prems 1);
+goal Fun.thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
 by (fast_tac (!claset addIs [inj_ontoI] 
                       addEs [inv_injective,injD]) 1);
 qed "inj_onto_inv";
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -278,7 +278,7 @@
 qed "less_SucE";
 
 goal thy "(m < Suc(n)) = (m < n | m = n)";
-by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
+by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1);
 qed "less_Suc_eq";
 
 val prems = goal thy "m<n ==> n ~= 0";
@@ -348,18 +348,18 @@
 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 [Suc_mono, less_SucI] addEs [lessE]) 1);
+by (blast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
 qed "less_linear";
 
 qed_goal "nat_less_cases" thy 
    "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
-( fn prems =>
+( fn [major,eqCase,lessCase] =>
         [
-        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
+        (rtac (less_linear RS disjE) 1),
         (etac disjE 2),
-        (etac (hd (tl (tl prems))) 1),
-        (etac (sym RS hd (tl prems)) 1),
-        (etac (hd prems) 1)
+        (etac lessCase 1),
+        (etac (sym RS eqCase) 1),
+        (etac major 1)
         ]);
 
 (*Can be used with less_Suc_eq to get n=m | n<m *)
@@ -511,19 +511,19 @@
 
 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
 by (dtac le_imp_less_or_eq 1);
-by (fast_tac (!claset addIs [less_trans]) 1);
+by (blast_tac (!claset addIs [less_trans]) 1);
 qed "le_less_trans";
 
 goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
 by (dtac le_imp_less_or_eq 1);
-by (fast_tac (!claset addIs [less_trans]) 1);
+by (blast_tac (!claset addIs [less_trans]) 1);
 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])]);
+	   blast_tac (!claset addIs [less_trans])]);
 qed "le_trans";
 
 goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
@@ -634,9 +634,9 @@
   (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 (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
+            blast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
                               addDs [less_trans_Suc]) 1,
-            atac 1]);
+            assume_tac 1]);
 val leD = le_eq_less_Suc RS iffD1;
 val not_lessD = nat_leI RS leD;
 val not_leD = not_leE
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Option.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -11,7 +11,7 @@
 val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
  br (prem RS rev_mp) 1;
  by (option.induct_tac "opt" 1);
- by (ALLGOALS(Fast_tac));
+ by (ALLGOALS Blast_tac);
 bind_thm("optionE", standard(result() RS disjE));
 (*
 goal Option.thy "opt=None | (? x.opt=Some(x))"; 
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Ord.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -25,26 +25,26 @@
 AddIffs [order_refl];
 
 goal Ord.thy "~ x < (x::'a::order)";
-by(simp_tac (!simpset addsimps [order_less_le]) 1);
+by (simp_tac (!simpset addsimps [order_less_le]) 1);
 qed "order_less_irrefl";
 AddIffs [order_less_irrefl];
 
 goal thy "(x::'a::order) <= y = (x < y | x = y)";
-by(simp_tac (!simpset addsimps [order_less_le]) 1);
-by(Fast_tac 1);
+by (simp_tac (!simpset addsimps [order_less_le]) 1);
+by (Blast_tac 1);
 qed "order_le_less";
 
 (** min **)
 
 goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by(split_tac [expand_if] 1);
-by(Asm_simp_tac 1);
+by (split_tac [expand_if] 1);
+by (Asm_simp_tac 1);
 qed "min_leastL";
 
 val prems = goalw thy [min_def]
  "(!!x::'a::order. least <= x) ==> min x least = least";
-by(cut_facts_tac prems 1);
-by(split_tac [expand_if] 1);
-by(Asm_simp_tac 1);
-by(fast_tac (!claset addEs [order_antisym]) 1);
+by (cut_facts_tac prems 1);
+by (split_tac [expand_if] 1);
+by (Asm_simp_tac 1);
+by (blast_tac (!claset addIs [order_antisym]) 1);
 qed "min_leastR";
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Prod.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -33,15 +33,15 @@
 AddSEs [Pair_inject];
 
 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Pair_eq";
 
 goalw Prod.thy [fst_def] "fst((a,b)) = a";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "fst_conv";
 
 goalw Prod.thy [snd_def] "snd((a,b)) = b";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "snd_conv";
 
 goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
@@ -119,12 +119,12 @@
 goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
 by (stac surjective_pairing 1);
 by (stac split 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "expand_split";
 
 (** split used as a logical connective or set former **)
 
-(*These rules are for use with fast_tac.
+(*These rules are for use with blast_tac.
   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
 
 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
@@ -193,8 +193,8 @@
 by (rtac (major RS imageE) 1);
 by (res_inst_tac [("p","x")] PairE 1);
 by (resolve_tac prems 1);
-by (Fast_tac 2);
-by (fast_tac (!claset addIs [prod_fun]) 1);
+by (Blast_tac 2);
+by (blast_tac (!claset addIs [prod_fun]) 1);
 qed "prod_fun_imageE";
 
 (*** Disjoint union of a family of sets - Sigma ***)
@@ -239,19 +239,19 @@
 val prems = goal Prod.thy
     "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "Sigma_mono";
 
 qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Sigma_empty1,Sigma_empty2]; 
 
 goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "mem_Sigma_iff";
 Addsimps [mem_Sigma_iff]; 
 
@@ -259,7 +259,7 @@
 (*Suggested by Pierre Chartier*)
 goal Prod.thy
      "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UNION_Times_distrib";
 
 (*** Domain of a relation ***)
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/RelPow.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -35,7 +35,7 @@
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
 by (cut_facts_tac [major] 1);
 by (Asm_full_simp_tac  1);
-by (fast_tac (!claset addIs [minor]) 1);
+by (blast_tac (!claset addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
 val [p1,p2,p3] = goal RelPow.thy
@@ -102,7 +102,7 @@
 qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
 
 
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Set.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -220,7 +220,7 @@
 
 qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
  (fn [prem]=>
-  [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
+  [ (blast_tac (!claset addIs [prem RS FalseE]) 1) ]);
 
 qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
  (fn _ => [ (Blast_tac 1) ]);
@@ -418,7 +418,7 @@
 (fn _ => [Blast_tac 1]);
 
 goal Set.thy "!!a b. {a}={b} ==> a=b";
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 qed "singleton_inject";
 
 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
@@ -622,11 +622,11 @@
 AddSEs [imageE]; 
 
 goalw thy [o_def] "(f o g)``r = f``(g``r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_compose";
 
 goal thy "f``(A Un B) = f``A Un f``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_Un";
 
 
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Trancl.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -52,7 +52,7 @@
 \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
 \  ==>  P((a,b))";
 by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "rtrancl_full_induct";
 
 (*nice induction rule*)
@@ -67,8 +67,8 @@
 by (Blast_tac 1);
 (*now do the induction*)
 by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (fast_tac (!claset addIs prems) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "rtrancl_induct";
 
 bind_thm
@@ -93,8 +93,8 @@
 \    |] ==> P";
 by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
 by (rtac (major RS rtrancl_induct) 2);
-by (fast_tac (!claset addIs prems) 2);
-by (fast_tac (!claset addIs prems) 2);
+by (blast_tac (!claset addIs prems) 2);
+by (blast_tac (!claset addIs prems) 2);
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
 qed "rtranclE";
 
@@ -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 addSDs[rtrancl_converseD])1);
+by (blast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
 qed "converse_rtrancl_induct";
 
 val prems = goal Trancl.thy
@@ -227,7 +227,7 @@
 (*now solve first subgoal: this formula is sufficient*)
 by (Blast_tac 1);
 by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
+by (ALLGOALS (blast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
 qed "trancl_induct";
 
 (*elimination of r^+ -- NOT an induction rule*)
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Univ.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/univ
+(*  Title:      HOL/Univ
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -147,7 +147,7 @@
 qed "Scons_inject_lemma1";
 
 goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
-by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/WF.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -27,7 +27,7 @@
 \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
 by (rtac (major RS spec RS mp RS spec) 1);
-by (fast_tac (!claset addEs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -38,9 +38,9 @@
 
 val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 by (wf_ind_tac "a" prems 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_asym";
 
 val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
@@ -58,8 +58,8 @@
 by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
 by (rtac (impI RS allI) 1);
 by (etac tranclE 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_trancl";
 
 
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/MT.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -17,30 +17,11 @@
 
 open MT;
 
-(*Limit cyclic unifications during monotonicity proofs*)
-val orig_search_bound = !Unify.search_bound;
-Unify.search_bound := 8;
-
-val prems = goal MT.thy "~a:{b} ==> ~a=b";
-by (cut_facts_tac prems 1);
-by (rtac notI 1);
-by (dtac notE 1);
-by (hyp_subst_tac 1);
-by (rtac singletonI 1);
-by (assume_tac 1);
-qed "notsingletonI";
-
 (* ############################################################ *)
 (* Inference systems                                            *)
 (* ############################################################ *)
 
-val infsys_mono_tac =
-  (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
-  (rtac CollectI 1) THEN (dtac CollectD 1) THEN
-  REPEAT 
-    ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
-      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
-    );
+val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
 
 val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
 by (simp_tac (!simpset addsimps prems) 1);
@@ -102,7 +83,7 @@
 by (rtac (monoh RS monoD) 1);
 by (rtac (UnE RS subsetI) 1);
 by (assume_tac 1);
-by (fast_tac (!claset addSIs [cih]) 1);
+by (blast_tac (!claset addSIs [cih]) 1);
 by (rtac (monoh RS monoD RS subsetD) 1);
 by (rtac Un_upper2 1);
 by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
@@ -169,7 +150,8 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (Fast_tac 1);
+	(*Naughty!  But the quantifiers are nested VERY deeply...*)
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "eval_const";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -178,7 +160,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "eval_var2";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -187,7 +169,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "eval_fn";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -197,7 +179,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "eval_fix";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -207,7 +189,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "eval_app1";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -220,7 +202,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (!claset addSIs [disjI2]) 1);
 qed "eval_app2";
 
 (* Strong elimination, induction on evaluations *)
@@ -250,7 +232,7 @@
 by (dtac CollectD 1);
 by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
 qed "eval_ind0";
 
 val prems = goal MT.thy 
@@ -287,51 +269,46 @@
 
 (* Introduction rules *)
 
-val prems = goalw MT.thy [elab_def, elab_rel_def] 
-  "c isof ty ==> te |- e_const(c) ===> ty";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def] 
+  "!!te. c isof ty ==> te |- e_const(c) ===> ty";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "elab_const";
 
-val prems = goalw MT.thy [elab_def, elab_rel_def] 
-  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def] 
+  "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "elab_var";
 
-val prems = goalw MT.thy [elab_def, elab_rel_def] 
-  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def] 
+  "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "elab_fn";
 
-val prems = goalw MT.thy [elab_def, elab_rel_def]
-  " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
-\   te |- fix f(x) = e ===> ty1->ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+  "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
+\        te |- fix f(x) = e ===> ty1->ty2";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
 qed "elab_fix";
 
-val prems = goalw MT.thy [elab_def, elab_rel_def] 
-  " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
-\   te |- e1 @ e2 ===> ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def] 
+  "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
+\        te |- e1 @ e2 ===> ty2";
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (!claset addSIs [disjI2]) 1);
 qed "elab_app";
 
 (* Strong elimination, induction on elaborations *)
@@ -361,7 +338,7 @@
 by (dtac CollectD 1);
 by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
 qed "elab_ind0";
 
 val prems = goal MT.thy
@@ -412,7 +389,7 @@
 by (dtac CollectD 1);
 by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
 qed "elab_elim0";
 
 val prems = goal MT.thy
@@ -441,7 +418,7 @@
 fun elab_e_elim_tac p = 
   ( (rtac elab_elim 1) THEN 
     (resolve_tac p 1) THEN 
-    (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
+    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
   );
 
 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
@@ -451,7 +428,7 @@
 val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
 by (cut_facts_tac prems 1);
 by (dtac elab_const_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "elab_const_elim";
 
 val prems = goal MT.thy 
@@ -463,7 +440,7 @@
   "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
 by (cut_facts_tac prems 1);
 by (dtac elab_var_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "elab_var_elim";
 
 val prems = goal MT.thy 
@@ -479,7 +456,7 @@
 \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
 by (cut_facts_tac prems 1);
 by (dtac elab_fn_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "elab_fn_elim";
 
 val prems = goal MT.thy 
@@ -494,7 +471,7 @@
 \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
 by (cut_facts_tac prems 1);
 by (dtac elab_fix_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "elab_fix_elim";
 
 val prems = goal MT.thy 
@@ -507,7 +484,7 @@
  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
 by (cut_facts_tac prems 1);
 by (dtac elab_app_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "elab_app_elim";
 
 (* ############################################################ *)
@@ -518,7 +495,8 @@
 
 goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
 by infsys_mono_tac;
-bind_thm("mono_hasty_fun",  result());
+by (Blast_tac 1);
+qed "mono_hasty_fun";
 
 (* 
   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
@@ -534,7 +512,7 @@
 by (rewtac MT.hasty_fun_def);
 by (rtac CollectI 1);
 by (rtac disjI1 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (rtac mono_hasty_fun 1);
 qed "hasty_rel_const_coind";
 
@@ -553,7 +531,7 @@
 by (rewtac hasty_fun_def);
 by (rtac CollectI 1);
 by (rtac disjI2 1);
-by (fast_tac (claset_of "HOL") 1);
+by (blast_tac HOL_cs 1);
 by (rtac mono_hasty_fun 1);
 qed "hasty_rel_clos_coind";
 
@@ -575,8 +553,7 @@
 by (dtac CollectD 1);
 by (fold_goals_tac [hasty_fun_def]);
 by (safe_tac (!claset));
-by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (REPEAT (ares_tac prems 1));
 qed "hasty_rel_elim0";
 
 val prems = goal MT.thy 
@@ -597,29 +574,27 @@
 
 (* Introduction rules for hasty *)
 
-val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
-by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
+goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
+by (etac hasty_rel_const_coind 1);
 qed "hasty_const";
 
-val prems = goalw MT.thy [hasty_def,hasty_env_def] 
-  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_def,hasty_env_def] 
+ "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
 by (rtac hasty_rel_clos_coind 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (blast_tac (!claset delrules [equalityI])));
 qed "hasty_clos";
 
 (* Elimination on constants for hasty *)
 
-val prems = goalw MT.thy [hasty_def] 
-  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_def] 
+  "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
 by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
+by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
 qed "hasty_elim_const_lem";
 
-val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
-by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
-by (Fast_tac 1);
+goal MT.thy "!!c. v_const(c) hasty t ==> c isof t";
+by (dtac hasty_elim_const_lem 1);
+by (Blast_tac 1);
 qed "hasty_elim_const";
 
 (* Elimination on closures for hasty *)
@@ -630,14 +605,14 @@
 \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
 by (cut_facts_tac prems 1);
 by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
+by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
 qed "hasty_elim_clos_lem";
 
-val prems = goal MT.thy 
-  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
-  \t & ve hastyenv te ";
-by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
-by (Fast_tac 1);
+goal MT.thy 
+  "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
+\       ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+by (dtac hasty_elim_clos_lem 1);
+by (Blast_tac 1);
 qed "hasty_elim_clos";
 
 (* ############################################################ *)
@@ -650,10 +625,10 @@
 by (rewtac hasty_env_def);
 by (asm_full_simp_tac (!simpset delsimps mem_simps
                                 addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
 by (excluded_middle_tac "ev=x" 1);
 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
 qed "hasty_env1";
 
@@ -661,38 +636,34 @@
 (* The Consistency theorem                                      *)
 (* ############################################################ *)
 
-val prems = goal MT.thy 
-  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
-by (cut_facts_tac prems 1);
+goal MT.thy 
+  "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
 by (dtac elab_const_elim 1);
 by (etac hasty_const 1);
 qed "consistency_const";
 
-val prems = goalw MT.thy [hasty_env_def]
-  " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
-\   ve_app ve ev hasty t";
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_env_def]
+  "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
+\       ve_app ve ev hasty t";
 by (dtac elab_var_elim 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "consistency_var";
 
-val prems = goal MT.thy
-  " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
-\   v_clos(<| ev, e, ve |>) hasty t";
-by (cut_facts_tac prems 1);
+goal MT.thy
+  "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+\       v_clos(<| ev, e, ve |>) hasty t";
 by (rtac hasty_clos 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "consistency_fn";
 
-val prems = goalw MT.thy [hasty_env_def,hasty_def]
-  " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
+goalw MT.thy [hasty_env_def,hasty_def]
+  "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
 \      ve hastyenv te ; \
 \      te |- fix ev2  ev1  = e ===> t \
 \   |] ==> \
 \   v_clos(cl) hasty t";
-by (cut_facts_tac prems 1);
 by (dtac elab_fix_elim 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
 (*Do a single unfolding of cl*)
 by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
 by (rtac hasty_rel_clos_coind 1);
@@ -700,37 +671,36 @@
 by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
 
 by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
 by (excluded_middle_tac "ev2=ev1a" 1);
 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 
 by (asm_simp_tac (!simpset delsimps mem_simps
                            addsimps [ve_app_owr1, te_app_owr1]) 1);
 by (hyp_subst_tac 1);
 by (etac subst 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "consistency_fix";
 
-val prems = goal MT.thy 
-  " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
+goal MT.thy 
+  "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
 \      ve hastyenv te ; te |- e1 @ e2 ===> t \
 \   |] ==> \
 \   v_const(c_app c1 c2) hasty t";
-by (cut_facts_tac prems 1);
 by (dtac elab_app_elim 1);
 by (safe_tac (!claset));
 by (rtac hasty_const 1);
 by (rtac isof_app 1);
 by (rtac hasty_elim_const 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (rtac hasty_elim_const 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "consistency_app1";
 
-val prems = goal MT.thy 
-  " [| ! t te. \
+goal MT.thy 
+  "!!t.  [| ! t te. \
 \        ve hastyenv te  --> \
 \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
@@ -740,7 +710,6 @@
 \      te |- e1 @ e2 ===> t \
 \   |] ==> \
 \   v hasty t";
-by (cut_facts_tac prems 1);
 by (dtac elab_app_elim 1);
 by (safe_tac (!claset));
 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
@@ -754,10 +723,7 @@
 by (dtac hasty_elim_clos 1);
 by (safe_tac (!claset));
 by (dtac elab_fn_elim 1);
-by (safe_tac (!claset));
-by (dtac t_fun_inj 1);
-by (safe_tac (!claset));
-by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
+by (blast_tac (!claset addIs [hasty_env1] addSDs [t_fun_inj]) 1);
 qed "consistency_app2";
 
 val [major] = goal MT.thy 
@@ -795,10 +761,7 @@
 by (cut_facts_tac prems 1);
 by (rtac hasty_elim_const 1);
 by (dtac consistency 1);
-by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
+by (blast_tac (!claset addSIs [basic_consistency_lem]) 1);
 qed "basic_consistency";
 
-
-Unify.search_bound := orig_search_bound;
-
 writeln"Reached end of file.";
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/Simult.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -29,7 +29,7 @@
 
 goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
+by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
                       addSEs [PartE]) 1);
 qed "TF_sexp";
 
@@ -50,7 +50,7 @@
 \            |] ==> R(FCONS M N)    \
 \    |] ==> R(i)";
 by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs (prems@[PartI])
+by (blast_tac (!claset addIs (prems@[PartI])
                        addEs [usumE, uprodE, PartE]) 1);
 qed "TF_induct";
 
@@ -59,13 +59,9 @@
  "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
 \                   (M: Part (TF A) In1 --> Q(M)) \
 \  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "TF_induct_lemma";
 
-AddSIs [PartI];
-AddSDs [In0_inject, In1_inject];
-AddSEs [PartE];
-
 (*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
 
 (*Induction on TF with separate predicates P, Q*)
@@ -93,12 +89,12 @@
     (Tree_Forest_induct RS conjE) 1);
 (*Instantiates ?A1 to range(Leaf). *)
 by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
-                             Rep_Forest_inverse RS subst] 
-                     addSIs [Rep_Tree,Rep_Forest]) 4);
+			      Rep_Forest_inverse RS subst] 
+                       addSIs [Rep_Tree,Rep_Forest]) 4);
 (*Cannot use simplifier: the rewrites work in the wrong direction!*)
 by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
-                          Abs_Forest_inverse RS subst] 
-                     addSIs prems)));
+					Abs_Forest_inverse RS subst] 
+                                addSIs prems)));
 qed "tree_forest_induct";
 
 
@@ -135,38 +131,38 @@
 AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
 AddSEs [Scons_inject];
 
-val prems = goalw Simult.thy TF_Rep_defs
-    "[| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
+by (Blast_tac 1);
 qed "TCONS_I";
 
 (* FNIL is a TF(A) -- this also justifies the type definition*)
 goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "FNIL_I";
 
-val prems = goalw Simult.thy TF_Rep_defs
-    "[| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
-\    FCONS M N : Part (TF A) In1";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
+\         FCONS M N : Part (TF A) In1";
+by (Blast_tac 1);
 qed "FCONS_I";
 
 (** Injectiveness of TCONS and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "TCONS_TCONS_eq";
 bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
 
 goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "FCONS_FCONS_eq";
 bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "TCONS_not_FNIL";
 bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
 
@@ -174,7 +170,7 @@
 val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "FCONS_not_FNIL";
 bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
 
@@ -182,7 +178,7 @@
 val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "TCONS_not_FCONS";
 bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
 
@@ -206,12 +202,12 @@
                            Leaf_inject];
 
 goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Tcons_Tcons_eq";
 bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
 
 goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Fcons_not_Fnil";
 
 bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
@@ -221,7 +217,7 @@
 (** Injectiveness of Fcons **)
 
 goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Fcons_Fcons_eq";
 bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
 
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/set.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -43,19 +43,18 @@
 
 (*** The Schroder-Berstein Theorem ***)
 
-val prems = goalw Lfp.thy [image_def] "inj(f) ==> inv(f)``(f``X) = X";
-by (cut_facts_tac prems 1);
+goalw Lfp.thy [image_def] "!!f. inj(f) ==> inv(f)``(f``X) = X";
 by (rtac equalityI 1);
 by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
 by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
 qed "inv_image_comp";
 
 goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "contra_imageI";
 
 goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "not_Compl";
 
 (*Lots of backtracking in this proof...*)
@@ -69,11 +68,11 @@
 goalw Lfp.thy [image_def]
     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "range_if_then_else";
 
 goal Lfp.thy "a : X Un Compl(X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "X_Un_Compl";
 
 goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
diff -r bd922fc9001b -r 998cb95fdd43 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/simpdata.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -55,7 +55,7 @@
 
 local
 
-  fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
 
   val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
   val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
@@ -118,7 +118,7 @@
 
 val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
-        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
+        (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
 
 (*Miniscoping: pushing in existential quantifiers*)
 val ex_simps = map prover 
@@ -153,7 +153,7 @@
 
 end;
 
-fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);
+fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
 
 prove "conj_commute" "(P&Q) = (Q&P)";
 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
@@ -196,19 +196,19 @@
 
 let val th = prove_goal HOL.thy 
                 "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
-                (fn _=> [fast_tac HOL_cs 1])
+                (fn _=> [blast_tac HOL_cs 1])
 in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
 
 let val th = prove_goal HOL.thy 
                 "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
-                (fn _=> [fast_tac HOL_cs 1])
+                (fn _=> [blast_tac HOL_cs 1])
 in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
 
 (* '|' congruence rule: not included by default! *)
 
 let val th = prove_goal HOL.thy 
                 "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
-                (fn _=> [fast_tac HOL_cs 1])
+                (fn _=> [blast_tac HOL_cs 1])
 in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
 
 prove "eq_sym_conv" "(x=y) = (y=x)";
@@ -220,10 +220,10 @@
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
- (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
 
 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
- (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
 
 qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
  (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -232,14 +232,14 @@
  (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
 *)
 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
- (fn _ => [fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
 
 qed_goal "expand_if" HOL.thy
     "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
  (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
          stac if_P 2,
          stac if_not_P 1,
-         REPEAT(fast_tac HOL_cs 1) ]);
+         REPEAT(blast_tac HOL_cs 1) ]);
 
 qed_goal "if_bool_eq" HOL.thy
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -257,7 +257,7 @@
 
 
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
-  (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
+  (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
 
 (** 'if' congruence rules: neither included by default! *)
 
@@ -267,7 +267,7 @@
 \  (if b then x else y) = (if c then u else v)"
   (fn rew::prems =>
    [stac rew 1, stac expand_if 1, stac expand_if 1,
-    fast_tac (HOL_cs addDs prems) 1]);
+    blast_tac (HOL_cs addDs prems) 1]);
 
 (*Prevents simplification of x and y: much faster*)
 qed_goal "if_weak_cong" HOL.thy