Using Blast_tac
authorpaulson
Wed Apr 09 12:32:04 1997 +0200 (1997-04-09)
changeset 2922580647a879cf
parent 2921 aee40b88a0ad
child 2923 f675fb52727b
Using Blast_tac
src/HOL/Arith.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/Shared.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ParRed.ML
src/HOL/NatDef.ML
src/HOL/RelPow.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/equalities.ML
src/HOL/ex/cla.ML
src/HOL/mono.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Apr 09 12:31:11 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Apr 09 12:32:04 1997 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  by (etac rev_mp 1);
     1.5  by (nat_ind_tac "k" 1);
     1.6  by (Simp_tac 1);
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  val lemma = result();
    1.10  
    1.11  (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.12 @@ -247,7 +247,7 @@
    1.13  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.14  goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    1.15  by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    1.16 -by (Fast_tac 1);
    1.17 +by (Blast_tac 1);
    1.18  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.19  by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    1.20  qed "diff_less";
    1.21 @@ -335,7 +335,7 @@
    1.22  
    1.23  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
    1.24  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
    1.25 -by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
    1.26 +by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
    1.27  qed "zero_induct_lemma";
    1.28  
    1.29  val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.30 @@ -385,7 +385,7 @@
    1.31  by (subgoal_tac "k mod 2 < 2" 1);
    1.32  by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
    1.33  by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.34 -by (Fast_tac 1);
    1.35 +by (Blast_tac 1);
    1.36  qed "mod2_cases";
    1.37  
    1.38  goal thy "Suc(Suc(m)) mod 2 = m mod 2";
    1.39 @@ -452,7 +452,7 @@
    1.40  by (etac rev_mp 1);
    1.41  by (nat_ind_tac "j" 1);
    1.42  by (ALLGOALS Asm_simp_tac);
    1.43 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
    1.44 +by (blast_tac (!claset addDs [Suc_lessD]) 1);
    1.45  qed "add_lessD1";
    1.46  
    1.47  goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
    1.48 @@ -468,7 +468,7 @@
    1.49  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.50  by (nat_ind_tac "k" 1);
    1.51  by (ALLGOALS Asm_simp_tac);
    1.52 -by (fast_tac (!claset addDs [Suc_leD]) 1);
    1.53 +by (blast_tac (!claset addDs [Suc_leD]) 1);
    1.54  qed_spec_mp "add_leD1";
    1.55  
    1.56  goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
    1.57 @@ -477,7 +477,7 @@
    1.58  qed_spec_mp "add_leD2";
    1.59  
    1.60  goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
    1.61 -by (fast_tac (!claset addDs [add_leD1, add_leD2]) 1);
    1.62 +by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
    1.63  bind_thm ("add_leE", result() RS conjE);
    1.64  
    1.65  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.66 @@ -513,7 +513,7 @@
    1.67  \     |] ==> f(i) <= (f(j)::nat)";
    1.68  by (cut_facts_tac [le] 1);
    1.69  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    1.70 -by (fast_tac (!claset addSIs [lt_mono]) 1);
    1.71 +by (blast_tac (!claset addSIs [lt_mono]) 1);
    1.72  qed "less_mono_imp_le_mono";
    1.73  
    1.74  (*non-strict, in 1st argument*)
     2.1 --- a/src/HOL/Auth/Message.ML	Wed Apr 09 12:31:11 1997 +0200
     2.2 +++ b/src/HOL/Auth/Message.ML	Wed Apr 09 12:32:04 1997 +0200
     2.3 @@ -188,7 +188,7 @@
     2.4  Addsimps [parts_Un, parts_UN, parts_UN1];
     2.5  
     2.6  goal thy "insert X (parts H) <= parts(insert X H)";
     2.7 -by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
     2.8 +by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
     2.9  qed "parts_insert_subset";
    2.10  
    2.11  (** Idempotence and transitivity **)
    2.12 @@ -196,8 +196,8 @@
    2.13  goal thy "!!H. X: parts (parts H) ==> X: parts H";
    2.14  by (etac parts.induct 1);
    2.15  by (ALLGOALS Blast_tac);
    2.16 -qed "parts_partsE";
    2.17 -AddSDs [parts_partsE];
    2.18 +qed "parts_partsD";
    2.19 +AddSDs [parts_partsD];
    2.20  
    2.21  goal thy "parts (parts H) = parts H";
    2.22  by (Blast_tac 1);
    2.23 @@ -255,7 +255,7 @@
    2.24  by (etac parts.induct 1);
    2.25  by (Auto_tac());
    2.26  by (etac parts.induct 1);
    2.27 -by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
    2.28 +by (ALLGOALS (blast_tac (!claset addIs [parts.Body])));
    2.29  qed "parts_insert_Crypt";
    2.30  
    2.31  goal thy "parts (insert {|X,Y|} H) = \
    2.32 @@ -265,7 +265,7 @@
    2.33  by (etac parts.induct 1);
    2.34  by (Auto_tac());
    2.35  by (etac parts.induct 1);
    2.36 -by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
    2.37 +by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd])));
    2.38  qed "parts_insert_MPair";
    2.39  
    2.40  Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
    2.41 @@ -350,7 +350,7 @@
    2.42  qed "analz_Un";
    2.43  
    2.44  goal thy "insert X (analz H) <= analz(insert X H)";
    2.45 -by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
    2.46 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    2.47  qed "analz_insert";
    2.48  
    2.49  (** Rewrite rules for pulling out atomic messages **)
    2.50 @@ -386,7 +386,7 @@
    2.51  by (etac analz.induct 1);
    2.52  by (Auto_tac());
    2.53  by (etac analz.induct 1);
    2.54 -by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd]) 0));
    2.55 +by (ALLGOALS (blast_tac (!claset addIs [analz.Fst, analz.Snd])));
    2.56  qed "analz_insert_MPair";
    2.57  
    2.58  (*Can pull out enCrypted message if the Key is not known*)
    2.59 @@ -410,7 +410,7 @@
    2.60  by (Auto_tac());
    2.61  by (eres_inst_tac [("za","x")] analz.induct 1);
    2.62  by (Auto_tac());
    2.63 -by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
    2.64 +by (blast_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
    2.65                               analz.Decrypt]) 1);
    2.66  val lemma2 = result();
    2.67  
    2.68 @@ -459,8 +459,8 @@
    2.69  goal thy "!!H. X: analz (analz H) ==> X: analz H";
    2.70  by (etac analz.induct 1);
    2.71  by (ALLGOALS Blast_tac);
    2.72 -qed "analz_analzE";
    2.73 -AddSDs [analz_analzE];
    2.74 +qed "analz_analzD";
    2.75 +AddSDs [analz_analzD];
    2.76  
    2.77  goal thy "analz (analz H) = analz H";
    2.78  by (Blast_tac 1);
    2.79 @@ -515,12 +515,11 @@
    2.80  (*Helps to prove Fake cases*)
    2.81  goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
    2.82  by (etac analz.induct 1);
    2.83 -by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
    2.84 +by (ALLGOALS (blast_tac (!claset addIs [impOfSubs analz_mono])));
    2.85  val lemma = result();
    2.86  
    2.87  goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
    2.88 -by (fast_tac (!claset addIs [lemma]
    2.89 -                      addEs [impOfSubs analz_mono]) 1);
    2.90 +by (blast_tac (!claset addIs [lemma, impOfSubs analz_mono]) 1);
    2.91  qed "analz_UN_analz";
    2.92  Addsimps [analz_UN_analz];
    2.93  
    2.94 @@ -561,7 +560,7 @@
    2.95  qed "synth_Un";
    2.96  
    2.97  goal thy "insert X (synth H) <= synth(insert X H)";
    2.98 -by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
    2.99 +by (blast_tac (!claset addIs [impOfSubs synth_mono]) 1);
   2.100  qed "synth_insert";
   2.101  
   2.102  (** Idempotence and transitivity **)
   2.103 @@ -569,8 +568,8 @@
   2.104  goal thy "!!H. X: synth (synth H) ==> X: synth H";
   2.105  by (etac synth.induct 1);
   2.106  by (ALLGOALS Blast_tac);
   2.107 -qed "synth_synthE";
   2.108 -AddSDs [synth_synthE];
   2.109 +qed "synth_synthD";
   2.110 +AddSDs [synth_synthD];
   2.111  
   2.112  goal thy "synth (synth H) = synth H";
   2.113  by (Blast_tac 1);
   2.114 @@ -620,7 +619,7 @@
   2.115  by (rtac subsetI 1);
   2.116  by (etac parts.induct 1);
   2.117  by (ALLGOALS
   2.118 -    (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
   2.119 +    (blast_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
   2.120                               ::parts.intrs))));
   2.121  qed "parts_synth";
   2.122  Addsimps [parts_synth];
   2.123 @@ -634,9 +633,8 @@
   2.124  by (rtac equalityI 1);
   2.125  by (rtac subsetI 1);
   2.126  by (etac analz.induct 1);
   2.127 -by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
   2.128 -(*Strange that best_tac just can't hack this one...*)
   2.129 -by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
   2.130 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 5);
   2.131 +by (ALLGOALS (blast_tac (!claset addIs analz.intrs)));
   2.132  qed "analz_synth_Un";
   2.133  
   2.134  goal thy "analz (synth H) = analz H Un synth H";
   2.135 @@ -651,8 +649,8 @@
   2.136  by (rtac equalityI 1);
   2.137  by (rtac subsetI 1);
   2.138  by (etac analz.induct 1);
   2.139 -by (best_tac
   2.140 -    (!claset addEs [impOfSubs synth_increasing,
   2.141 +by (blast_tac
   2.142 +    (!claset addIs [impOfSubs synth_increasing,
   2.143                      impOfSubs analz_mono]) 5);
   2.144  by (Blast_tac 1);
   2.145  by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
   2.146 @@ -691,8 +689,8 @@
   2.147  \              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
   2.148  by (rtac subsetI 1);
   2.149  by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
   2.150 -by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   2.151 -                      addSEs [impOfSubs analz_mono]) 2);
   2.152 +by (blast_tac (!claset addIs [impOfSubs analz_mono,
   2.153 +			      impOfSubs (analz_mono RS synth_mono)]) 2);
   2.154  by (Full_simp_tac 1);
   2.155  by (Blast_tac 1);
   2.156  qed "Fake_analz_insert";
     3.1 --- a/src/HOL/Auth/Shared.ML	Wed Apr 09 12:31:11 1997 +0200
     3.2 +++ b/src/HOL/Auth/Shared.ML	Wed Apr 09 12:32:04 1997 +0200
     3.3 @@ -424,5 +424,5 @@
     3.4  goal thy  
     3.5   "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
     3.6  \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
     3.7 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
     3.8 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
     3.9  qed "analz_image_freshK_lemma";
     4.1 --- a/src/HOL/Finite.ML	Wed Apr 09 12:31:11 1997 +0200
     4.2 +++ b/src/HOL/Finite.ML	Wed Apr 09 12:32:04 1997 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4  qed "Fin_mono";
     4.5  
     4.6  goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
     4.7 -by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
     4.8 +by (blast_tac (!claset addSIs [lfp_lowerbound]) 1);
     4.9  qed "Fin_subset_Pow";
    4.10  
    4.11  (* A : Fin(B) ==> A <= B *)
    4.12 @@ -55,7 +55,7 @@
    4.13  qed "Fin_subset";
    4.14  
    4.15  goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
    4.16 -by (fast_tac (!claset addIs [Fin_UnI] addDs
    4.17 +by (blast_tac (!claset addIs [Fin_UnI] addDs
    4.18                  [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    4.19  qed "subset_Fin";
    4.20  Addsimps[subset_Fin];
    4.21 @@ -63,7 +63,7 @@
    4.22  goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    4.23  by (stac insert_is_Un 1);
    4.24  by (Simp_tac 1);
    4.25 -by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
    4.26 +by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
    4.27  qed "insert_Fin";
    4.28  Addsimps[insert_Fin];
    4.29  
    4.30 @@ -163,7 +163,7 @@
    4.31  section "Finite cardinality -- 'card'";
    4.32  
    4.33  goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    4.34 -by (Fast_tac 1);
    4.35 +by (Blast_tac 1);
    4.36  val Collect_conv_insert = result();
    4.37  
    4.38  goalw Finite.thy [card_def] "card {} = 0";
    4.39 @@ -197,7 +197,7 @@
    4.40  by (case_tac "? a. a:A" 1);
    4.41   by (res_inst_tac [("x","0")] exI 2);
    4.42   by (Simp_tac 2);
    4.43 - by (Fast_tac 2);
    4.44 + by (Blast_tac 2);
    4.45  by (etac exE 1);
    4.46  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    4.47  by (rtac exI 1);
    4.48 @@ -205,47 +205,47 @@
    4.49  by (etac equalityE 1);
    4.50  by (asm_full_simp_tac
    4.51       (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    4.52 -by (SELECT_GOAL(safe_tac (!claset))1);
    4.53 +by (safe_tac (!claset));
    4.54    by (Asm_full_simp_tac 1);
    4.55    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    4.56    by (SELECT_GOAL(safe_tac (!claset))1);
    4.57     by (subgoal_tac "x ~= f m" 1);
    4.58 -    by (Fast_tac 2);
    4.59 +    by (Blast_tac 2);
    4.60     by (subgoal_tac "? k. f k = x & k<m" 1);
    4.61 -    by (best_tac (!claset) 2);
    4.62 +    by (Blast_tac 2);
    4.63     by (SELECT_GOAL(safe_tac (!claset))1);
    4.64     by (res_inst_tac [("x","k")] exI 1);
    4.65     by (Asm_simp_tac 1);
    4.66    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.67 -  by (best_tac (!claset) 1);
    4.68 +  by (Blast_tac 1);
    4.69   bd sym 1;
    4.70   by (rotate_tac ~1 1);
    4.71   by (Asm_full_simp_tac 1);
    4.72   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    4.73   by (SELECT_GOAL(safe_tac (!claset))1);
    4.74    by (subgoal_tac "x ~= f m" 1);
    4.75 -   by (Fast_tac 2);
    4.76 +   by (Blast_tac 2);
    4.77    by (subgoal_tac "? k. f k = x & k<m" 1);
    4.78 -   by (best_tac (!claset) 2);
    4.79 +   by (Blast_tac 2);
    4.80    by (SELECT_GOAL(safe_tac (!claset))1);
    4.81    by (res_inst_tac [("x","k")] exI 1);
    4.82    by (Asm_simp_tac 1);
    4.83   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.84 - by (best_tac (!claset) 1);
    4.85 + by (Blast_tac 1);
    4.86  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    4.87  by (SELECT_GOAL(safe_tac (!claset))1);
    4.88   by (subgoal_tac "x ~= f i" 1);
    4.89 -  by (Fast_tac 2);
    4.90 +  by (Blast_tac 2);
    4.91   by (case_tac "x = f m" 1);
    4.92    by (res_inst_tac [("x","i")] exI 1);
    4.93    by (Asm_simp_tac 1);
    4.94   by (subgoal_tac "? k. f k = x & k<m" 1);
    4.95 -  by (best_tac (!claset) 2);
    4.96 +  by (Blast_tac 2);
    4.97   by (SELECT_GOAL(safe_tac (!claset))1);
    4.98   by (res_inst_tac [("x","k")] exI 1);
    4.99   by (Asm_simp_tac 1);
   4.100  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   4.101 -by (best_tac (!claset) 1);
   4.102 +by (Blast_tac 1);
   4.103  val lemma = result();
   4.104  
   4.105  goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
   4.106 @@ -303,8 +303,8 @@
   4.107  by (Asm_simp_tac 1);
   4.108  by (rtac card_insert_disjoint 1);
   4.109  by (rtac (major RSN (2,finite_subset)) 1);
   4.110 -by (Fast_tac 1);
   4.111 -by (Fast_tac 1);
   4.112 +by (Blast_tac 1);
   4.113 +by (Blast_tac 1);
   4.114  by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
   4.115  qed "card_insert";
   4.116  Addsimps [card_insert];
     5.1 --- a/src/HOL/Fun.ML	Wed Apr 09 12:31:11 1997 +0200
     5.2 +++ b/src/HOL/Fun.ML	Wed Apr 09 12:32:04 1997 +0200
     5.3 @@ -99,11 +99,9 @@
     5.4  
     5.5  (*** Lemmas about inj ***)
     5.6  
     5.7 -val prems = goalw Fun.thy [o_def]
     5.8 -    "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
     5.9 -by (cut_facts_tac prems 1);
    5.10 -by (fast_tac (!claset addIs [injI]
    5.11 -                     addEs [injD,inj_ontoD]) 1);
    5.12 +goalw Fun.thy [o_def]
    5.13 +    "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    5.14 +by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1);
    5.15  qed "comp_inj";
    5.16  
    5.17  val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
     6.1 --- a/src/HOL/Lambda/Commutation.ML	Wed Apr 09 12:31:11 1997 +0200
     6.2 +++ b/src/HOL/Lambda/Commutation.ML	Wed Apr 09 12:32:04 1997 +0200
     6.3 @@ -94,6 +94,6 @@
     6.4         rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
     6.5  by (etac rtrancl_induct 1);
     6.6   by (Blast_tac 1);
     6.7 -by (slow_best_tac (!claset addIs [r_into_rtrancl]
     6.8 -                    addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
     6.9 +by (blast_tac (!claset delrules [rtrancl_refl] 
    6.10 +                       addIs [r_into_rtrancl, rtrancl_trans]) 1);
    6.11  qed "Church_Rosser_confluent";
     7.1 --- a/src/HOL/Lambda/Eta.ML	Wed Apr 09 12:31:11 1997 +0200
     7.2 +++ b/src/HOL/Lambda/Eta.ML	Wed Apr 09 12:32:04 1997 +0200
     7.3 @@ -80,10 +80,9 @@
     7.4  by (etac eta.induct 1);
     7.5  by (slow_tac (!claset addIs [subst_not_free,eta_subst]
     7.6                        addIs [free_eta RS iffD1] addss !simpset) 1);
     7.7 -by (slow_tac (!claset) 1);
     7.8 -by (slow_tac (!claset) 1);
     7.9 -by (slow_tac (!claset addSIs [eta_subst]
    7.10 -                           addIs [free_eta RS iffD1]) 1);
    7.11 +by (safe_tac (!claset));
    7.12 +by (blast_tac (!claset addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
    7.13 +by (ALLGOALS Blast_tac);
    7.14  qed "square_eta";
    7.15  
    7.16  goal Eta.thy "confluent(eta)";
    7.17 @@ -108,8 +107,8 @@
    7.18  qed "rtrancl_eta_AppR";
    7.19  
    7.20  goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
    7.21 -by (deepen_tac (!claset addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
    7.22 -                     addIs [rtrancl_trans]) 2 1);
    7.23 +by (blast_tac (!claset addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
    7.24 +                       addIs [rtrancl_trans]) 1);
    7.25  qed "rtrancl_eta_App";
    7.26  
    7.27  section "Commutation of -> and -e>";
    7.28 @@ -152,8 +151,9 @@
    7.29  by (etac beta.induct 1);
    7.30  by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
    7.31                        addss !simpset) 1);
    7.32 -by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
    7.33 -by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
    7.34 +by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 6 1);
    7.35 +by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 6 1);
    7.36 +(*23 seconds?*)
    7.37  by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
    7.38                        addss !simpset) 1);
    7.39  qed "square_beta_eta";
     8.1 --- a/src/HOL/Lambda/Lambda.ML	Wed Apr 09 12:31:11 1997 +0200
     8.2 +++ b/src/HOL/Lambda/Lambda.ML	Wed Apr 09 12:32:04 1997 +0200
     8.3 @@ -38,8 +38,8 @@
     8.4  qed "rtrancl_beta_AppR";
     8.5  
     8.6  goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
     8.7 -by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
     8.8 -                        addIs  [rtrancl_trans]) 3 1);
     8.9 +by (blast_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
    8.10 +                       addIs  [rtrancl_trans]) 1);
    8.11  qed "rtrancl_beta_App";
    8.12  AddIs [rtrancl_beta_App];
    8.13  
    8.14 @@ -90,8 +90,8 @@
    8.15  by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
    8.16                                  setloop (split_tac [expand_if])
    8.17                                  addSolver cut_trans_tac)));
    8.18 -by(safe_tac (HOL_cs addSEs [nat_neqE]));
    8.19 -by(ALLGOALS trans_tac);
    8.20 +by (safe_tac (HOL_cs addSEs [nat_neqE]));
    8.21 +by (ALLGOALS trans_tac);
    8.22  qed "lift_subst_lt";
    8.23  
    8.24  goal Lambda.thy "!k s. (lift t k)[s/k] = t";
    8.25 @@ -108,8 +108,8 @@
    8.26        (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
    8.27                  setloop (split_tac [expand_if,expand_nat_case])
    8.28                  addSolver cut_trans_tac)));
    8.29 -by(safe_tac (HOL_cs addSEs [nat_neqE]));
    8.30 -by(ALLGOALS trans_tac);
    8.31 +by (safe_tac (HOL_cs addSEs [nat_neqE]));
    8.32 +by (ALLGOALS trans_tac);
    8.33  qed_spec_mp "subst_subst";
    8.34  
    8.35  
     9.1 --- a/src/HOL/Lambda/ParRed.ML	Wed Apr 09 12:31:11 1997 +0200
     9.2 +++ b/src/HOL/Lambda/ParRed.ML	Wed Apr 09 12:32:04 1997 +0200
     9.3 @@ -43,8 +43,10 @@
     9.4  by (rtac subsetI 1);
     9.5  by (split_all_tac 1);
     9.6  by (etac par_beta.induct 1);
     9.7 -by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl] 
     9.8 -                                     addEs [rtrancl_trans])));
     9.9 +by (Blast_tac 1);
    9.10 +(* rtrancl_refl complicates the proof by increasing the branching factor*)
    9.11 +by (ALLGOALS (blast_tac (!claset delrules [rtrancl_refl]
    9.12 +				 addIs [rtrancl_into_rtrancl])));
    9.13  qed "par_beta_subset_beta";
    9.14  
    9.15  (*** => ***)
    9.16 @@ -72,7 +74,7 @@
    9.17  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    9.18  by (rtac (impI RS allI RS allI) 1);
    9.19  by (etac par_beta.induct 1);
    9.20 -by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
    9.21 +by (ALLGOALS(blast_tac (!claset addSIs [par_beta_subst])));
    9.22  qed "diamond_par_beta";
    9.23  
    9.24  
    9.25 @@ -90,7 +92,7 @@
    9.26  (*** Confluence (via cd) ***)
    9.27  
    9.28  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    9.29 -by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
    9.30 +by (blast_tac (!claset addIs [par_beta_cd]) 1);
    9.31  qed "diamond_par_beta2";
    9.32  
    9.33  goal ParRed.thy "confluent(beta)";
    10.1 --- a/src/HOL/NatDef.ML	Wed Apr 09 12:31:11 1997 +0200
    10.2 +++ b/src/HOL/NatDef.ML	Wed Apr 09 12:32:04 1997 +0200
    10.3 @@ -278,7 +278,7 @@
    10.4  qed "less_SucE";
    10.5  
    10.6  goal thy "(m < Suc(n)) = (m < n | m = n)";
    10.7 -by (fast_tac (!claset addEs  [less_trans, less_SucE]) 1);
    10.8 +by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
    10.9  qed "less_Suc_eq";
   10.10  
   10.11  val prems = goal thy "m<n ==> n ~= 0";
    11.1 --- a/src/HOL/RelPow.ML	Wed Apr 09 12:31:11 1997 +0200
    11.2 +++ b/src/HOL/RelPow.ML	Wed Apr 09 12:32:04 1997 +0200
    11.3 @@ -17,14 +17,14 @@
    11.4  
    11.5  goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    11.6  by (Simp_tac  1);
    11.7 -by (Fast_tac 1);
    11.8 +by (Blast_tac 1);
    11.9  qed "rel_pow_Suc_I";
   11.10  
   11.11  goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
   11.12  by (nat_ind_tac "n" 1);
   11.13  by (Simp_tac  1);
   11.14  by (Asm_full_simp_tac 1);
   11.15 -by (Fast_tac 1);
   11.16 +by (Blast_tac 1);
   11.17  qed_spec_mp "rel_pow_Suc_I2";
   11.18  
   11.19  goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
   11.20 @@ -53,8 +53,8 @@
   11.21  
   11.22  goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
   11.23  by (nat_ind_tac "n" 1);
   11.24 -by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
   11.25 -by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
   11.26 +by (blast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
   11.27 +by (blast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
   11.28  qed_spec_mp "rel_pow_Suc_D2";
   11.29  
   11.30  
   11.31 @@ -86,13 +86,14 @@
   11.32  goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
   11.33  by (split_all_tac 1);
   11.34  by (etac rtrancl_induct 1);
   11.35 -by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
   11.36 +by (ALLGOALS (blast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
   11.37  qed "rtrancl_imp_UN_rel_pow";
   11.38  
   11.39  goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
   11.40  by (nat_ind_tac "n" 1);
   11.41 -by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
   11.42 -by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
   11.43 +by (blast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
   11.44 +by (blast_tac (!claset addEs [rel_pow_Suc_E]
   11.45 +	               addIs [rtrancl_into_rtrancl]) 1);
   11.46  val lemma = result() RS spec RS mp;
   11.47  
   11.48  goal RelPow.thy "!!p. p:R^n ==> p:R^*";
    12.1 --- a/src/HOL/Sum.ML	Wed Apr 09 12:31:11 1997 +0200
    12.2 +++ b/src/HOL/Sum.ML	Wed Apr 09 12:32:04 1997 +0200
    12.3 @@ -185,7 +185,7 @@
    12.4  qed "Part_subset";
    12.5  
    12.6  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
    12.7 -by (Fast_tac 1);
    12.8 +by (Blast_tac 1);
    12.9  qed "Part_mono";
   12.10  
   12.11  val basic_monos = basic_monos @ [Part_mono];
   12.12 @@ -199,10 +199,10 @@
   12.13  qed "Part_id";
   12.14  
   12.15  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
   12.16 -by (Fast_tac 1);
   12.17 +by (Blast_tac 1);
   12.18  qed "Part_Int";
   12.19  
   12.20  (*For inductive definitions*)
   12.21  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
   12.22 -by (Fast_tac 1);
   12.23 +by (Blast_tac 1);
   12.24  qed "Part_Collect";
    13.1 --- a/src/HOL/Trancl.ML	Wed Apr 09 12:31:11 1997 +0200
    13.2 +++ b/src/HOL/Trancl.ML	Wed Apr 09 12:32:04 1997 +0200
    13.3 @@ -80,7 +80,7 @@
    13.4  goalw Trancl.thy [trans_def] "trans(r^*)";
    13.5  by (safe_tac (!claset));
    13.6  by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    13.7 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
    13.8 +by (ALLGOALS(blast_tac (!claset addIs [rtrancl_into_rtrancl])));
    13.9  qed "trans_rtrancl";
   13.10  
   13.11  bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
   13.12 @@ -110,7 +110,7 @@
   13.13  by (rtac iffI 1);
   13.14  by (etac rtrancl_induct 1);
   13.15  by (rtac rtrancl_refl 1);
   13.16 -by (fast_tac (!claset addEs [rtrancl_trans]) 1);
   13.17 +by (blast_tac (!claset addIs [rtrancl_trans]) 1);
   13.18  by (etac r_into_rtrancl 1);
   13.19  qed "rtrancl_idemp";
   13.20  Addsimps [rtrancl_idemp];
   13.21 @@ -128,13 +128,13 @@
   13.22  qed "rtrancl_subset";
   13.23  
   13.24  goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
   13.25 -by (best_tac (!claset addSIs [rtrancl_subset]
   13.26 -                      addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   13.27 +by (blast_tac (!claset addSIs [rtrancl_subset]
   13.28 +                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   13.29  qed "rtrancl_Un_rtrancl";
   13.30  
   13.31  goal Trancl.thy "(R^=)^* = R^*";
   13.32 -by (fast_tac (!claset addSIs [rtrancl_refl,rtrancl_subset]
   13.33 -                      addIs  [r_into_rtrancl]) 1);
   13.34 +by (blast_tac (!claset addSIs [rtrancl_subset]
   13.35 +                       addIs  [rtrancl_refl, r_into_rtrancl]) 1);
   13.36  qed "rtrancl_reflcl";
   13.37  Addsimps [rtrancl_reflcl];
   13.38  
   13.39 @@ -142,14 +142,14 @@
   13.40  by (rtac converseI 1);
   13.41  by (etac rtrancl_induct 1);
   13.42  by (rtac rtrancl_refl 1);
   13.43 -by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
   13.44 +by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
   13.45  qed "rtrancl_converseD";
   13.46  
   13.47  goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
   13.48  by (dtac converseD 1);
   13.49  by (etac rtrancl_induct 1);
   13.50  by (rtac rtrancl_refl 1);
   13.51 -by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
   13.52 +by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
   13.53  qed "rtrancl_converseI";
   13.54  
   13.55  goal Trancl.thy "(converse r)^* = converse(r^*)";
   13.56 @@ -241,7 +241,7 @@
   13.57  by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   13.58  by (etac rtranclE 1);
   13.59  by (Blast_tac 1);
   13.60 -by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
   13.61 +by (blast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
   13.62  qed "tranclE";
   13.63  
   13.64  (*Transitivity of r^+.
    14.1 --- a/src/HOL/equalities.ML	Wed Apr 09 12:31:11 1997 +0200
    14.2 +++ b/src/HOL/equalities.ML	Wed Apr 09 12:32:04 1997 +0200
    14.3 @@ -30,7 +30,7 @@
    14.4  qed "insert_is_Un";
    14.5  
    14.6  goal Set.thy "insert a A ~= {}";
    14.7 -by (fast_tac (!claset addEs [equalityCE]) 1);
    14.8 +by (blast_tac (!claset addEs [equalityCE]) 1);
    14.9  qed"insert_not_empty";
   14.10  Addsimps[insert_not_empty];
   14.11  
   14.12 @@ -152,11 +152,11 @@
   14.13  qed "Int_Un_distrib2";
   14.14  
   14.15  goal Set.thy "(A<=B) = (A Int B = A)";
   14.16 -by (fast_tac (!claset addSEs [equalityE]) 1);
   14.17 +by (blast_tac (!claset addSEs [equalityE]) 1);
   14.18  qed "subset_Int_eq";
   14.19  
   14.20  goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
   14.21 -by (fast_tac (!claset addEs [equalityCE]) 1);
   14.22 +by (blast_tac (!claset addEs [equalityCE]) 1);
   14.23  qed "Int_UNIV";
   14.24  Addsimps[Int_UNIV];
   14.25  
   14.26 @@ -213,7 +213,7 @@
   14.27  qed "Un_Int_crazy";
   14.28  
   14.29  goal Set.thy "(A<=B) = (A Un B = B)";
   14.30 -by (fast_tac (!claset addSEs [equalityE]) 1);
   14.31 +by (blast_tac (!claset addSEs [equalityE]) 1);
   14.32  qed "subset_Un_eq";
   14.33  
   14.34  goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
   14.35 @@ -221,7 +221,7 @@
   14.36  qed "subset_insert_iff";
   14.37  
   14.38  goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   14.39 -by (fast_tac (!claset addEs [equalityCE]) 1);
   14.40 +by (blast_tac (!claset addEs [equalityCE]) 1);
   14.41  qed "Un_empty";
   14.42  Addsimps[Un_empty];
   14.43  
   14.44 @@ -260,7 +260,7 @@
   14.45  (*Halmos, Naive Set Theory, page 16.*)
   14.46  
   14.47  goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   14.48 -by (fast_tac (!claset addSEs [equalityE]) 1);
   14.49 +by (blast_tac (!claset addSEs [equalityE]) 1);
   14.50  qed "Un_Int_assoc_eq";
   14.51  
   14.52  
   14.53 @@ -292,7 +292,7 @@
   14.54  
   14.55  val prems = goal Set.thy
   14.56     "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
   14.57 -by (fast_tac (!claset addSEs [equalityE]) 1);
   14.58 +by (blast_tac (!claset addSEs [equalityE]) 1);
   14.59  qed "Union_disjoint";
   14.60  
   14.61  section "Inter";
   14.62 @@ -517,8 +517,8 @@
   14.63  qed "insert_Diff1";
   14.64  Addsimps [insert_Diff1];
   14.65  
   14.66 -val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   14.67 -by (fast_tac (!claset addSIs prems) 1);
   14.68 +goal Set.thy "!!a. a:A ==> insert a (A-{a}) = A";
   14.69 +by (Blast_tac 1);
   14.70  qed "insert_Diff";
   14.71  
   14.72  goal Set.thy "A Int (B-A) = {}";
    15.1 --- a/src/HOL/ex/cla.ML	Wed Apr 09 12:31:11 1997 +0200
    15.2 +++ b/src/HOL/ex/cla.ML	Wed Apr 09 12:32:04 1997 +0200
    15.3 @@ -424,7 +424,7 @@
    15.4  \  (!x. hates agatha x --> hates butler x) & \
    15.5  \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
    15.6  \   killed ?who agatha";
    15.7 -by (Blast_tac 1);
    15.8 +by (Fast_tac 1);
    15.9  result();
   15.10  
   15.11  writeln"Problem 56";
    16.1 --- a/src/HOL/mono.ML	Wed Apr 09 12:31:11 1997 +0200
    16.2 +++ b/src/HOL/mono.ML	Wed Apr 09 12:32:04 1997 +0200
    16.3 @@ -7,62 +7,62 @@
    16.4  *)
    16.5  
    16.6  goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
    16.7 -by (Fast_tac 1);
    16.8 +by (Blast_tac 1);
    16.9  qed "image_mono";
   16.10  
   16.11  goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
   16.12 -by (Fast_tac 1);
   16.13 +by (Blast_tac 1);
   16.14  qed "Pow_mono";
   16.15  
   16.16  goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
   16.17 -by (Fast_tac 1);
   16.18 +by (Blast_tac 1);
   16.19  qed "Union_mono";
   16.20  
   16.21  goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
   16.22 -by (Fast_tac 1);
   16.23 +by (Blast_tac 1);
   16.24  qed "Inter_anti_mono";
   16.25  
   16.26  val prems = goal Set.thy
   16.27      "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   16.28  \    (UN x:A. f(x)) <= (UN x:B. g(x))";
   16.29 -by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
   16.30 +by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
   16.31  qed "UN_mono";
   16.32  
   16.33  val [prem] = goal Set.thy
   16.34      "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
   16.35 -by (fast_tac (!claset addIs [prem RS subsetD]) 1);
   16.36 +by (blast_tac (!claset addIs [prem RS subsetD]) 1);
   16.37  qed "UN1_mono";
   16.38  
   16.39  val prems = goal Set.thy
   16.40      "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   16.41  \    (INT x:A. f(x)) <= (INT x:A. g(x))";
   16.42 -by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
   16.43 +by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
   16.44  qed "INT_anti_mono";
   16.45  
   16.46  (*The inclusion is POSITIVE! *)
   16.47  val [prem] = goal Set.thy
   16.48      "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
   16.49 -by (fast_tac (!claset addIs [prem RS subsetD]) 1);
   16.50 +by (blast_tac (!claset addIs [prem RS subsetD]) 1);
   16.51  qed "INT1_mono";
   16.52  
   16.53  goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
   16.54 -by (Fast_tac 1);
   16.55 +by (Blast_tac 1);
   16.56  qed "insert_mono";
   16.57  
   16.58  goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
   16.59 -by (Fast_tac 1);
   16.60 +by (Blast_tac 1);
   16.61  qed "Un_mono";
   16.62  
   16.63  goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
   16.64 -by (Fast_tac 1);
   16.65 +by (Blast_tac 1);
   16.66  qed "Int_mono";
   16.67  
   16.68  goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
   16.69 -by (Fast_tac 1);
   16.70 +by (Blast_tac 1);
   16.71  qed "Diff_mono";
   16.72  
   16.73  goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
   16.74 -by (Fast_tac 1);
   16.75 +by (Blast_tac 1);
   16.76  qed "Compl_anti_mono";
   16.77  
   16.78  (** Monotonicity of implications.  For inductive definitions **)
   16.79 @@ -74,15 +74,15 @@
   16.80  qed "in_mono";
   16.81  
   16.82  goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
   16.83 -by (Fast_tac 1);
   16.84 +by (Blast_tac 1);
   16.85  qed "conj_mono";
   16.86  
   16.87  goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
   16.88 -by (Fast_tac 1);
   16.89 +by (Blast_tac 1);
   16.90  qed "disj_mono";
   16.91  
   16.92  goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
   16.93 -by (Fast_tac 1);
   16.94 +by (Blast_tac 1);
   16.95  qed "imp_mono";
   16.96  
   16.97  goal HOL.thy "P-->P";
   16.98 @@ -92,24 +92,24 @@
   16.99  
  16.100  val [PQimp] = goal HOL.thy
  16.101      "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
  16.102 -by (fast_tac (!claset addIs [PQimp RS mp]) 1);
  16.103 +by (blast_tac (!claset addIs [PQimp RS mp]) 1);
  16.104  qed "ex_mono";
  16.105  
  16.106  val [PQimp] = goal HOL.thy
  16.107      "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
  16.108 -by (fast_tac (!claset addIs [PQimp RS mp]) 1);
  16.109 +by (blast_tac (!claset addIs [PQimp RS mp]) 1);
  16.110  qed "all_mono";
  16.111  
  16.112  val [PQimp] = goal Set.thy
  16.113      "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
  16.114 -by (fast_tac (!claset addIs [PQimp RS mp]) 1);
  16.115 +by (blast_tac (!claset addIs [PQimp RS mp]) 1);
  16.116  qed "Collect_mono";
  16.117  
  16.118  (*Used in indrule.ML*)
  16.119  val [subs,PQimp] = goal Set.thy
  16.120      "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
  16.121  \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
  16.122 -by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
  16.123 +by (blast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
  16.124  qed "Int_Collect_mono";
  16.125  
  16.126  (*Used in intr_elim.ML and in individual datatype definitions*)
    17.1 --- a/src/HOL/thy_syntax.ML	Wed Apr 09 12:31:11 1997 +0200
    17.2 +++ b/src/HOL/thy_syntax.ML	Wed Apr 09 12:32:04 1997 +0200
    17.3 @@ -120,7 +120,8 @@
    17.4    fun mk_params ((ts, tname), cons) =
    17.5     ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
    17.6      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    17.7 -    \val thy = thy",
    17.8 +    \val thy = thy"
    17.9 +    ,
   17.10      "structure " ^ tname ^ " =\n\
   17.11      \struct\n\
   17.12      \ val inject = map (get_axiom thy) " ^
   17.13 @@ -172,6 +173,7 @@
   17.14  
   17.15  (** primrec **)
   17.16  
   17.17 +(*recursion equations have user-supplied names*)
   17.18  fun mk_primrec_decl_1 ((fname, tname), axms) =
   17.19    let
   17.20      (*Isolate type name from the structure's identifier it may be stored in*)
   17.21 @@ -184,10 +186,13 @@
   17.22        \  (fn _ => [Simp_tac 1]));";
   17.23  
   17.24      val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   17.25 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
   17.26 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs
   17.27 +      , 
   17.28 +      cat_lines (map mk_prove axms)
   17.29        ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   17.30    end;
   17.31  
   17.32 +(*recursion equations have no names*)
   17.33  fun mk_primrec_decl_2 ((fname, tname), axms) =
   17.34    let
   17.35      (*Isolate type name from the structure's identifier it may be stored in*)
   17.36 @@ -199,17 +204,44 @@
   17.37        \(fn _ => [Simp_tac 1])";
   17.38  
   17.39      val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
   17.40 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
   17.41 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs
   17.42 +      ,
   17.43        "val dummy = Addsimps " ^
   17.44        brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
   17.45    end;
   17.46  
   17.47 +(*function name, argument type and either (name,axiom) pairs or just axioms*)
   17.48  val primrec_decl =
   17.49    (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
   17.50    (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
   17.51  
   17.52  
   17.53  
   17.54 +
   17.55 +(** rec: interface to Slind's TFL **)
   17.56 +
   17.57 +
   17.58 +fun mk_rec_decl ((fname, rel), axms) =
   17.59 +  let val fid = trim fname
   17.60 +  in
   17.61 +	 (";\n\n\
   17.62 +          \structure " ^ fid ^ " =\n\
   17.63 +          \  struct\n\
   17.64 +          \  val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   17.65 +          \  val {induct,eqns,thy,tcs} = Tfl.RfuncStringList " ^ 
   17.66 +	                 rel ^ "\n" ^ mk_big_list axms ^ " thy;\n\
   17.67 +          \  end;\n\n\
   17.68 +          \val thy = thy"
   17.69 +         ,
   17.70 +	 "")
   17.71 +  end;
   17.72 +
   17.73 +val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
   17.74 +
   17.75 +
   17.76 +
   17.77 +
   17.78 +
   17.79  (** sections **)
   17.80  
   17.81  val user_keywords = ["intrs", "monos", "con_defs", "|"];
   17.82 @@ -219,7 +251,8 @@
   17.83    ("inductive", inductive_decl ""),
   17.84    ("coinductive", inductive_decl "Co"),
   17.85    ("datatype", datatype_decl),
   17.86 -  ("primrec", primrec_decl)];
   17.87 +  ("primrec", primrec_decl),
   17.88 +  ("recdef", rec_decl)];
   17.89  
   17.90  
   17.91  end;