# HG changeset patch
# User paulson
# Date 860581924 -7200
# Node ID 580647a879cf1c92c422be7649f5758f029c33a2
# Parent  aee40b88a0ad6b90722e417c71bbdbaaa1ad1b1d
Using Blast_tac

diff -r aee40b88a0ad -r 580647a879cf src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Arith.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -50,7 +50,7 @@
 by (etac rev_mp 1);
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 val lemma = result();
 
 (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
@@ -247,7 +247,7 @@
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
 qed "diff_less";
@@ -335,7 +335,7 @@
 
 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
+by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
 qed "zero_induct_lemma";
 
 val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
@@ -385,7 +385,7 @@
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "mod2_cases";
 
 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
@@ -452,7 +452,7 @@
 by (etac rev_mp 1);
 by (nat_ind_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
 qed "add_lessD1";
 
 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
@@ -468,7 +468,7 @@
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [Suc_leD]) 1);
+by (blast_tac (!claset addDs [Suc_leD]) 1);
 qed_spec_mp "add_leD1";
 
 goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
@@ -477,7 +477,7 @@
 qed_spec_mp "add_leD2";
 
 goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
-by (fast_tac (!claset addDs [add_leD1, add_leD2]) 1);
+by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
 bind_thm ("add_leE", result() RS conjE);
 
 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
@@ -513,7 +513,7 @@
 \     |] ==> f(i) <= (f(j)::nat)";
 by (cut_facts_tac [le] 1);
 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-by (fast_tac (!claset addSIs [lt_mono]) 1);
+by (blast_tac (!claset addSIs [lt_mono]) 1);
 qed "less_mono_imp_le_mono";
 
 (*non-strict, in 1st argument*)
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -188,7 +188,7 @@
 Addsimps [parts_Un, parts_UN, parts_UN1];
 
 goal thy "insert X (parts H) <= parts(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
 qed "parts_insert_subset";
 
 (** Idempotence and transitivity **)
@@ -196,8 +196,8 @@
 goal thy "!!H. X: parts (parts H) ==> X: parts H";
 by (etac parts.induct 1);
 by (ALLGOALS Blast_tac);
-qed "parts_partsE";
-AddSDs [parts_partsE];
+qed "parts_partsD";
+AddSDs [parts_partsD];
 
 goal thy "parts (parts H) = parts H";
 by (Blast_tac 1);
@@ -255,7 +255,7 @@
 by (etac parts.induct 1);
 by (Auto_tac());
 by (etac parts.induct 1);
-by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
+by (ALLGOALS (blast_tac (!claset addIs [parts.Body])));
 qed "parts_insert_Crypt";
 
 goal thy "parts (insert {|X,Y|} H) = \
@@ -265,7 +265,7 @@
 by (etac parts.induct 1);
 by (Auto_tac());
 by (etac parts.induct 1);
-by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
+by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd])));
 qed "parts_insert_MPair";
 
 Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
@@ -350,7 +350,7 @@
 qed "analz_Un";
 
 goal thy "insert X (analz H) <= analz(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
 qed "analz_insert";
 
 (** Rewrite rules for pulling out atomic messages **)
@@ -386,7 +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]) 0));
+by (ALLGOALS (blast_tac (!claset addIs [analz.Fst, analz.Snd])));
 qed "analz_insert_MPair";
 
 (*Can pull out enCrypted message if the Key is not known*)
@@ -410,7 +410,7 @@
 by (Auto_tac());
 by (eres_inst_tac [("za","x")] analz.induct 1);
 by (Auto_tac());
-by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
+by (blast_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
                              analz.Decrypt]) 1);
 val lemma2 = result();
 
@@ -459,8 +459,8 @@
 goal thy "!!H. X: analz (analz H) ==> X: analz H";
 by (etac analz.induct 1);
 by (ALLGOALS Blast_tac);
-qed "analz_analzE";
-AddSDs [analz_analzE];
+qed "analz_analzD";
+AddSDs [analz_analzD];
 
 goal thy "analz (analz H) = analz H";
 by (Blast_tac 1);
@@ -515,12 +515,11 @@
 (*Helps to prove Fake cases*)
 goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
 by (etac analz.induct 1);
-by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
+by (ALLGOALS (blast_tac (!claset addIs [impOfSubs analz_mono])));
 val lemma = result();
 
 goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
-by (fast_tac (!claset addIs [lemma]
-                      addEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [lemma, impOfSubs analz_mono]) 1);
 qed "analz_UN_analz";
 Addsimps [analz_UN_analz];
 
@@ -561,7 +560,7 @@
 qed "synth_Un";
 
 goal thy "insert X (synth H) <= synth(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs synth_mono]) 1);
 qed "synth_insert";
 
 (** Idempotence and transitivity **)
@@ -569,8 +568,8 @@
 goal thy "!!H. X: synth (synth H) ==> X: synth H";
 by (etac synth.induct 1);
 by (ALLGOALS Blast_tac);
-qed "synth_synthE";
-AddSDs [synth_synthE];
+qed "synth_synthD";
+AddSDs [synth_synthD];
 
 goal thy "synth (synth H) = synth H";
 by (Blast_tac 1);
@@ -620,7 +619,7 @@
 by (rtac subsetI 1);
 by (etac parts.induct 1);
 by (ALLGOALS
-    (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
+    (blast_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
                              ::parts.intrs))));
 qed "parts_synth";
 Addsimps [parts_synth];
@@ -634,9 +633,8 @@
 by (rtac equalityI 1);
 by (rtac subsetI 1);
 by (etac analz.induct 1);
-by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
-(*Strange that best_tac just can't hack this one...*)
-by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 5);
+by (ALLGOALS (blast_tac (!claset addIs analz.intrs)));
 qed "analz_synth_Un";
 
 goal thy "analz (synth H) = analz H Un synth H";
@@ -651,8 +649,8 @@
 by (rtac equalityI 1);
 by (rtac subsetI 1);
 by (etac analz.induct 1);
-by (best_tac
-    (!claset addEs [impOfSubs synth_increasing,
+by (blast_tac
+    (!claset addIs [impOfSubs synth_increasing,
                     impOfSubs analz_mono]) 5);
 by (Blast_tac 1);
 by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
@@ -691,8 +689,8 @@
 \              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
 by (rtac subsetI 1);
 by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
-by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
-                      addSEs [impOfSubs analz_mono]) 2);
+by (blast_tac (!claset addIs [impOfSubs analz_mono,
+			      impOfSubs (analz_mono RS synth_mono)]) 2);
 by (Full_simp_tac 1);
 by (Blast_tac 1);
 qed "Fake_analz_insert";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -424,5 +424,5 @@
 goal thy  
  "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
 \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
 qed "analz_image_freshK_lemma";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Finite.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -16,7 +16,7 @@
 qed "Fin_mono";
 
 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
+by (blast_tac (!claset addSIs [lfp_lowerbound]) 1);
 qed "Fin_subset_Pow";
 
 (* A : Fin(B) ==> A <= B *)
@@ -55,7 +55,7 @@
 qed "Fin_subset";
 
 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (fast_tac (!claset addIs [Fin_UnI] addDs
+by (blast_tac (!claset addIs [Fin_UnI] addDs
                 [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
 qed "subset_Fin";
 Addsimps[subset_Fin];
@@ -63,7 +63,7 @@
 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
 by (stac insert_is_Un 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
+by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
 qed "insert_Fin";
 Addsimps[insert_Fin];
 
@@ -163,7 +163,7 @@
 section "Finite cardinality -- 'card'";
 
 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 val Collect_conv_insert = result();
 
 goalw Finite.thy [card_def] "card {} = 0";
@@ -197,7 +197,7 @@
 by (case_tac "? a. a:A" 1);
  by (res_inst_tac [("x","0")] exI 2);
  by (Simp_tac 2);
- by (Fast_tac 2);
+ by (Blast_tac 2);
 by (etac exE 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
@@ -205,47 +205,47 @@
 by (etac equalityE 1);
 by (asm_full_simp_tac
      (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
-by (SELECT_GOAL(safe_tac (!claset))1);
+by (safe_tac (!claset));
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   by (SELECT_GOAL(safe_tac (!claset))1);
    by (subgoal_tac "x ~= f m" 1);
-    by (Fast_tac 2);
+    by (Blast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
-    by (best_tac (!claset) 2);
+    by (Blast_tac 2);
    by (SELECT_GOAL(safe_tac (!claset))1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-  by (best_tac (!claset) 1);
+  by (Blast_tac 1);
  bd sym 1;
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
  by (SELECT_GOAL(safe_tac (!claset))1);
   by (subgoal_tac "x ~= f m" 1);
-   by (Fast_tac 2);
+   by (Blast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
-   by (best_tac (!claset) 2);
+   by (Blast_tac 2);
   by (SELECT_GOAL(safe_tac (!claset))1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (best_tac (!claset) 1);
+ by (Blast_tac 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
 by (SELECT_GOAL(safe_tac (!claset))1);
  by (subgoal_tac "x ~= f i" 1);
-  by (Fast_tac 2);
+  by (Blast_tac 2);
  by (case_tac "x = f m" 1);
   by (res_inst_tac [("x","i")] exI 1);
   by (Asm_simp_tac 1);
  by (subgoal_tac "? k. f k = x & k<m" 1);
-  by (best_tac (!claset) 2);
+  by (Blast_tac 2);
  by (SELECT_GOAL(safe_tac (!claset))1);
  by (res_inst_tac [("x","k")] exI 1);
  by (Asm_simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
@@ -303,8 +303,8 @@
 by (Asm_simp_tac 1);
 by (rtac card_insert_disjoint 1);
 by (rtac (major RSN (2,finite_subset)) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
 qed "card_insert";
 Addsimps [card_insert];
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Fun.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -99,11 +99,9 @@
 
 (*** Lemmas about inj ***)
 
-val prems = goalw Fun.thy [o_def]
-    "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
-by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [injI]
-                     addEs [injD,inj_ontoD]) 1);
+goalw Fun.thy [o_def]
+    "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
+by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1);
 qed "comp_inj";
 
 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -94,6 +94,6 @@
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (etac rtrancl_induct 1);
  by (Blast_tac 1);
-by (slow_best_tac (!claset addIs [r_into_rtrancl]
-                    addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
+by (blast_tac (!claset delrules [rtrancl_refl] 
+                       addIs [r_into_rtrancl, rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -80,10 +80,9 @@
 by (etac eta.induct 1);
 by (slow_tac (!claset addIs [subst_not_free,eta_subst]
                       addIs [free_eta RS iffD1] addss !simpset) 1);
-by (slow_tac (!claset) 1);
-by (slow_tac (!claset) 1);
-by (slow_tac (!claset addSIs [eta_subst]
-                           addIs [free_eta RS iffD1]) 1);
+by (safe_tac (!claset));
+by (blast_tac (!claset addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
+by (ALLGOALS Blast_tac);
 qed "square_eta";
 
 goal Eta.thy "confluent(eta)";
@@ -108,8 +107,8 @@
 qed "rtrancl_eta_AppR";
 
 goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
-by (deepen_tac (!claset addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
-                     addIs [rtrancl_trans]) 2 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
+                       addIs [rtrancl_trans]) 1);
 qed "rtrancl_eta_App";
 
 section "Commutation of -> and -e>";
@@ -152,8 +151,9 @@
 by (etac beta.induct 1);
 by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
                       addss !simpset) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
+by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 6 1);
+by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 6 1);
+(*23 seconds?*)
 by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
                       addss !simpset) 1);
 qed "square_beta_eta";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -38,8 +38,8 @@
 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]
-                        addIs  [rtrancl_trans]) 3 1);
+by (blast_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
+                       addIs  [rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
 AddIs [rtrancl_beta_App];
 
@@ -90,8 +90,8 @@
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
                                 setloop (split_tac [expand_if])
                                 addSolver cut_trans_tac)));
-by(safe_tac (HOL_cs addSEs [nat_neqE]));
-by(ALLGOALS trans_tac);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
 qed "lift_subst_lt";
 
 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
@@ -108,8 +108,8 @@
       (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
                 setloop (split_tac [expand_if,expand_nat_case])
                 addSolver cut_trans_tac)));
-by(safe_tac (HOL_cs addSEs [nat_neqE]));
-by(ALLGOALS trans_tac);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
 qed_spec_mp "subst_subst";
 
 
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -43,8 +43,10 @@
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac par_beta.induct 1);
-by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl] 
-                                     addEs [rtrancl_trans])));
+by (Blast_tac 1);
+(* rtrancl_refl complicates the proof by increasing the branching factor*)
+by (ALLGOALS (blast_tac (!claset delrules [rtrancl_refl]
+				 addIs [rtrancl_into_rtrancl])));
 qed "par_beta_subset_beta";
 
 (*** => ***)
@@ -72,7 +74,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(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
+by (ALLGOALS(blast_tac (!claset addSIs [par_beta_subst])));
 qed "diamond_par_beta";
 
 
@@ -90,7 +92,7 @@
 (*** Confluence (via cd) ***)
 
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
+by (blast_tac (!claset addIs [par_beta_cd]) 1);
 qed "diamond_par_beta2";
 
 goal ParRed.thy "confluent(beta)";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Apr 09 12:32:04 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 (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
 qed "less_Suc_eq";
 
 val prems = goal thy "m<n ==> n ~= 0";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/RelPow.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -17,14 +17,14 @@
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
 by (Simp_tac  1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by (nat_ind_tac "n" 1);
 by (Simp_tac  1);
 by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
@@ -53,8 +53,8 @@
 
 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by (nat_ind_tac "n" 1);
-by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 
@@ -86,13 +86,14 @@
 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
 by (split_all_tac 1);
 by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
+by (ALLGOALS (blast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
 qed "rtrancl_imp_UN_rel_pow";
 
 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
 by (nat_ind_tac "n" 1);
-by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
+by (blast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (blast_tac (!claset addEs [rel_pow_Suc_E]
+	               addIs [rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Sum.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -185,7 +185,7 @@
 qed "Part_subset";
 
 goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Part_mono";
 
 val basic_monos = basic_monos @ [Part_mono];
@@ -199,10 +199,10 @@
 qed "Part_id";
 
 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (Fast_tac 1);
+by (Blast_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 1);
+by (Blast_tac 1);
 qed "Part_Collect";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Trancl.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -80,7 +80,7 @@
 goalw Trancl.thy [trans_def] "trans(r^*)";
 by (safe_tac (!claset));
 by (eres_inst_tac [("b","z")] rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "trans_rtrancl";
 
 bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
@@ -110,7 +110,7 @@
 by (rtac iffI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (!claset addEs [rtrancl_trans]) 1);
+by (blast_tac (!claset addIs [rtrancl_trans]) 1);
 by (etac r_into_rtrancl 1);
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
@@ -128,13 +128,13 @@
 qed "rtrancl_subset";
 
 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by (best_tac (!claset addSIs [rtrancl_subset]
-                      addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
+by (blast_tac (!claset addSIs [rtrancl_subset]
+                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
 qed "rtrancl_Un_rtrancl";
 
 goal Trancl.thy "(R^=)^* = R^*";
-by (fast_tac (!claset addSIs [rtrancl_refl,rtrancl_subset]
-                      addIs  [r_into_rtrancl]) 1);
+by (blast_tac (!claset addSIs [rtrancl_subset]
+                       addIs  [rtrancl_refl, r_into_rtrancl]) 1);
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
@@ -142,14 +142,14 @@
 by (rtac converseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseD";
 
 goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
 by (dtac converseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(converse r)^* = converse(r^*)";
@@ -241,7 +241,7 @@
 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
 by (etac rtranclE 1);
 by (Blast_tac 1);
-by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
+by (blast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
 qed "tranclE";
 
 (*Transitivity of r^+.
diff -r aee40b88a0ad -r 580647a879cf src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/equalities.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -30,7 +30,7 @@
 qed "insert_is_Un";
 
 goal Set.thy "insert a A ~= {}";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
 qed"insert_not_empty";
 Addsimps[insert_not_empty];
 
@@ -152,11 +152,11 @@
 qed "Int_Un_distrib2";
 
 goal Set.thy "(A<=B) = (A Int B = A)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_eq";
 
 goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
@@ -213,7 +213,7 @@
 qed "Un_Int_crazy";
 
 goal Set.thy "(A<=B) = (A Un B = B)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_eq";
 
 goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
@@ -221,7 +221,7 @@
 qed "subset_insert_iff";
 
 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
 qed "Un_empty";
 Addsimps[Un_empty];
 
@@ -260,7 +260,7 @@
 (*Halmos, Naive Set Theory, page 16.*)
 
 goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Un_Int_assoc_eq";
 
 
@@ -292,7 +292,7 @@
 
 val prems = goal Set.thy
    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
 section "Inter";
@@ -517,8 +517,8 @@
 qed "insert_Diff1";
 Addsimps [insert_Diff1];
 
-val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
-by (fast_tac (!claset addSIs prems) 1);
+goal Set.thy "!!a. a:A ==> insert a (A-{a}) = A";
+by (Blast_tac 1);
 qed "insert_Diff";
 
 goal Set.thy "A Int (B-A) = {}";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/ex/cla.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -424,7 +424,7 @@
 \  (!x. hates agatha x --> hates butler x) & \
 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
 \   killed ?who agatha";
-by (Blast_tac 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 56";
diff -r aee40b88a0ad -r 580647a879cf src/HOL/mono.ML
--- a/src/HOL/mono.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/mono.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -7,62 +7,62 @@
 *)
 
 goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "image_mono";
 
 goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Pow_mono";
 
 goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_mono";
 
 goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Inter_anti_mono";
 
 val prems = goal Set.thy
     "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (UN x:A. f(x)) <= (UN x:B. g(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "UN_mono";
 
 val [prem] = goal Set.thy
     "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
-by (fast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem RS subsetD]) 1);
 qed "UN1_mono";
 
 val prems = goal Set.thy
     "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (INT x:A. f(x)) <= (INT x:A. g(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "INT_anti_mono";
 
 (*The inclusion is POSITIVE! *)
 val [prem] = goal Set.thy
     "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
-by (fast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem RS subsetD]) 1);
 qed "INT1_mono";
 
 goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "insert_mono";
 
 goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Un_mono";
 
 goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Int_mono";
 
 goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Diff_mono";
 
 goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Compl_anti_mono";
 
 (** Monotonicity of implications.  For inductive definitions **)
@@ -74,15 +74,15 @@
 qed "in_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "conj_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "disj_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "imp_mono";
 
 goal HOL.thy "P-->P";
@@ -92,24 +92,24 @@
 
 val [PQimp] = goal HOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "ex_mono";
 
 val [PQimp] = goal HOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "all_mono";
 
 val [PQimp] = goal Set.thy
     "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "Collect_mono";
 
 (*Used in indrule.ML*)
 val [subs,PQimp] = goal Set.thy
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
 \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
-by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
 qed "Int_Collect_mono";
 
 (*Used in intr_elim.ML and in individual datatype definitions*)
diff -r aee40b88a0ad -r 580647a879cf src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/thy_syntax.ML	Wed Apr 09 12:32:04 1997 +0200
@@ -120,7 +120,8 @@
   fun mk_params ((ts, tname), cons) =
    ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
-    \val thy = thy",
+    \val thy = thy"
+    ,
     "structure " ^ tname ^ " =\n\
     \struct\n\
     \ val inject = map (get_axiom thy) " ^
@@ -172,6 +173,7 @@
 
 (** primrec **)
 
+(*recursion equations have user-supplied names*)
 fun mk_primrec_decl_1 ((fname, tname), axms) =
   let
     (*Isolate type name from the structure's identifier it may be stored in*)
@@ -184,10 +186,13 @@
       \  (fn _ => [Simp_tac 1]));";
 
     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
-  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
+  in ("|> " ^ tname ^ "_add_primrec " ^ axs
+      , 
+      cat_lines (map mk_prove axms)
       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   end;
 
+(*recursion equations have no names*)
 fun mk_primrec_decl_2 ((fname, tname), axms) =
   let
     (*Isolate type name from the structure's identifier it may be stored in*)
@@ -199,17 +204,44 @@
       \(fn _ => [Simp_tac 1])";
 
     val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
-  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
+  in ("|> " ^ tname ^ "_add_primrec " ^ axs
+      ,
       "val dummy = Addsimps " ^
       brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
   end;
 
+(*function name, argument type and either (name,axiom) pairs or just axioms*)
 val primrec_decl =
   (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
   (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
 
 
 
+
+(** rec: interface to Slind's TFL **)
+
+
+fun mk_rec_decl ((fname, rel), axms) =
+  let val fid = trim fname
+  in
+	 (";\n\n\
+          \structure " ^ fid ^ " =\n\
+          \  struct\n\
+          \  val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
+          \  val {induct,eqns,thy,tcs} = Tfl.RfuncStringList " ^ 
+	                 rel ^ "\n" ^ mk_big_list axms ^ " thy;\n\
+          \  end;\n\n\
+          \val thy = thy"
+         ,
+	 "")
+  end;
+
+val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
+
+
+
+
+
 (** sections **)
 
 val user_keywords = ["intrs", "monos", "con_defs", "|"];
@@ -219,7 +251,8 @@
   ("inductive", inductive_decl ""),
   ("coinductive", inductive_decl "Co"),
   ("datatype", datatype_decl),
-  ("primrec", primrec_decl)];
+  ("primrec", primrec_decl),
+  ("recdef", rec_decl)];
 
 
 end;