renamed less_eq_Suc_add to less_imp_Suc_add
authorpaulson
Fri Dec 01 11:02:55 2000 +0100 (2000-12-01)
changeset 1055809a91221ced1
parent 10557 dc615fccc1e6
child 10559 d3fd54fc659b
renamed less_eq_Suc_add to less_imp_Suc_add
src/HOL/Integ/IntDef.ML
src/HOL/Nat.ML
src/HOL/Real/Hyperreal/SEQ.ML
src/HOL/Real/Hyperreal/Series.ML
src/HOL/ex/Primrec.ML
     1.1 --- a/src/HOL/Integ/IntDef.ML	Thu Nov 30 20:18:00 2000 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Fri Dec 01 11:02:55 2000 +0100
     1.3 @@ -351,7 +351,7 @@
     1.4  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
     1.5  by (Clarify_tac 1);
     1.6  by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
     1.7 -by (safe_tac (claset() addSDs [less_eq_Suc_add]));
     1.8 +by (safe_tac (claset() addSDs [less_imp_Suc_add]));
     1.9  by (res_inst_tac [("x","k")] exI 1);
    1.10  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
    1.11  qed "zless_iff_Suc_zadd";
     2.1 --- a/src/HOL/Nat.ML	Thu Nov 30 20:18:00 2000 +0100
     2.2 +++ b/src/HOL/Nat.ML	Fri Dec 01 11:02:55 2000 +0100
     2.3 @@ -265,13 +265,13 @@
     2.4  
     2.5  (**** Additional theorems about "less than" ****)
     2.6  
     2.7 -(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
     2.8 +(*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
     2.9  Goal "m<n --> (EX k. n=Suc(m+k))";
    2.10  by (induct_tac "n" 1);
    2.11  by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
    2.12  by (blast_tac (claset() addSEs [less_SucE]
    2.13                          addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    2.14 -qed_spec_mp "less_eq_Suc_add";
    2.15 +qed_spec_mp "less_imp_Suc_add";
    2.16  
    2.17  Goal "n <= ((m + n)::nat)";
    2.18  by (induct_tac "m" 1);
    2.19 @@ -288,7 +288,7 @@
    2.20  bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
    2.21  
    2.22  Goal "(m<n) = (EX k. n=Suc(m+k))";
    2.23 -by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
    2.24 +by (blast_tac (claset() addSIs [less_add_Suc1, less_imp_Suc_add]) 1);
    2.25  qed "less_iff_Suc_add";
    2.26  
    2.27  
    2.28 @@ -634,7 +634,7 @@
    2.29  
    2.30  (*strict, in 1st argument; proof is by induction on k>0*)
    2.31  Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
    2.32 -by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
    2.33 +by (eres_inst_tac [("m1","0")] (less_imp_Suc_add RS exE) 1);
    2.34  by (Asm_simp_tac 1);
    2.35  by (induct_tac "x" 1);
    2.36  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
     3.1 --- a/src/HOL/Real/Hyperreal/SEQ.ML	Thu Nov 30 20:18:00 2000 +0100
     3.2 +++ b/src/HOL/Real/Hyperreal/SEQ.ML	Fri Dec 01 11:02:55 2000 +0100
     3.3 @@ -120,7 +120,7 @@
     3.4  by (induct_tac "u" 1);
     3.5  by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
     3.6  by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
     3.7 -    finite_nat_le_segment],simpset()));
     3.8 +    finite_nat_le_segment], simpset()));
     3.9  by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
    3.10  by (ALLGOALS(Asm_simp_tac));
    3.11  qed "NSLIMSEQ_finite_set";
    3.12 @@ -153,7 +153,7 @@
    3.13  Goal "{n. abs (X (f n) + - L) < r} Int \
    3.14  \         {n. r <= abs (X (f n) + - (L::real))} = {}";
    3.15  by (auto_tac (claset() addDs [real_less_le_trans] 
    3.16 -    addIs [real_less_irrefl],simpset()));
    3.17 +    addIs [real_less_irrefl], simpset()));
    3.18  val lemmaLIM2 = result();
    3.19  
    3.20  Goal "!!f. [| #0 < r; ALL n. r <= abs (X (f n) + - L); \
    3.21 @@ -323,7 +323,7 @@
    3.22        "!!X. [| X ----NS> a; X ----NS> b |] \
    3.23  \           ==> a = b";
    3.24  by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
    3.25 -by (auto_tac (claset() addDs [inf_close_trans3],simpset()));
    3.26 +by (auto_tac (claset() addDs [inf_close_trans3], simpset()));
    3.27  qed "NSLIMSEQ_unique";
    3.28  
    3.29  Goal "!!X. [| X ----> a; X ----> b |] \
    3.30 @@ -377,21 +377,21 @@
    3.31  
    3.32  Goalw [NSconvergent_def,nslim_def] 
    3.33        "NSconvergent X = (X ----NS> nslim X)";
    3.34 -by (auto_tac (claset() addIs [someI],simpset()));
    3.35 +by (auto_tac (claset() addIs [someI], simpset()));
    3.36  qed "NSconvergent_NSLIMSEQ_iff";
    3.37  
    3.38  Goalw [convergent_def,lim_def] 
    3.39        "convergent X = (X ----> lim X)";
    3.40 -by (auto_tac (claset() addIs [someI],simpset()));
    3.41 +by (auto_tac (claset() addIs [someI], simpset()));
    3.42  qed "convergent_LIMSEQ_iff";
    3.43  
    3.44  (*-------------------------------------------------------------------
    3.45           Subsequence (alternative definition) (e.g. Hoskins)
    3.46   ------------------------------------------------------------------*)
    3.47  Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
    3.48 -by (auto_tac (claset() addSDs [less_eq_Suc_add],simpset()));
    3.49 +by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
    3.50  by (nat_ind_tac "k" 1);
    3.51 -by (auto_tac (claset() addIs [less_trans],simpset()));
    3.52 +by (auto_tac (claset() addIs [less_trans], simpset()));
    3.53  qed "subseq_Suc_iff";
    3.54  
    3.55  (*-------------------------------------------------------------------
    3.56 @@ -403,13 +403,14 @@
    3.57  \                | (ALL n. X (Suc n) <= X n))";
    3.58  by (auto_tac (claset () addSDs [le_imp_less_or_eq],
    3.59      simpset() addsimps [real_le_refl]));
    3.60 -by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
    3.61 -    addSDs [less_eq_Suc_add],simpset()));
    3.62 +by (auto_tac (claset() addSIs [lessI RS less_imp_le]
    3.63 +                       addSDs [less_imp_Suc_add], 
    3.64 +    simpset()));
    3.65  by (induct_tac "ka" 1);
    3.66 -by (auto_tac (claset() addIs [real_le_trans],simpset()));
    3.67 +by (auto_tac (claset() addIs [real_le_trans], simpset()));
    3.68  by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
    3.69  by (induct_tac "k" 1);
    3.70 -by (auto_tac (claset() addIs [real_le_trans],simpset()));
    3.71 +by (auto_tac (claset() addIs [real_le_trans], simpset()));
    3.72  qed "monoseq_Suc";
    3.73  
    3.74  Goalw [monoseq_def] 
    3.75 @@ -568,7 +569,7 @@
    3.76            RS finite_subset) 1);
    3.77  by (rtac finite_real_of_posnat_less_real 1);
    3.78  by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
    3.79 -by (auto_tac (claset() addIs [finite_real_of_posnat_less_real],simpset()));
    3.80 +by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset()));
    3.81  val lemma_finite_NSBseq2 = result();
    3.82  
    3.83  Goal "ALL N. real_of_posnat  N < abs (X (f N)) \
    3.84 @@ -765,7 +766,7 @@
    3.85  
    3.86  Goalw [convergent_def] 
    3.87        "!!X. (convergent X) = (convergent (%n. -(X n)))";
    3.88 -by (auto_tac (claset() addDs [LIMSEQ_minus],simpset()));
    3.89 +by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
    3.90  by (dtac LIMSEQ_minus 1 THEN Auto_tac);
    3.91  qed "convergent_minus_iff";
    3.92  
    3.93 @@ -781,7 +782,7 @@
    3.94  by (Step_tac 1);
    3.95  by (rtac (convergent_minus_iff RS ssubst) 2);
    3.96  by (dtac (Bseq_minus_iff RS ssubst) 2);
    3.97 -by (auto_tac (claset() addSIs [Bseq_mono_convergent],simpset()));
    3.98 +by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
    3.99  qed "Bseq_monoseq_convergent";
   3.100  
   3.101  (*----------------------------------------------------------------
   3.102 @@ -815,7 +816,7 @@
   3.103  by (res_inst_tac [("j","abs(X n) + abs (X N)")] 
   3.104      real_le_trans 1);
   3.105  by (auto_tac (claset() addIs [abs_triangle_minus_ineq,
   3.106 -    real_add_le_mono1],simpset() addsimps [Bseq_iff2]));
   3.107 +    real_add_le_mono1], simpset() addsimps [Bseq_iff2]));
   3.108  qed "Bseq_iff3";
   3.109  
   3.110  val real_not_leE = CLAIM "~ m <= n ==> n < (m::real)";
   3.111 @@ -830,7 +831,7 @@
   3.112  by (res_inst_tac [("j","abs K")] real_le_trans 1);
   3.113  by (res_inst_tac [("j","abs k")] real_le_trans 3);
   3.114  by (auto_tac (claset() addSIs [rename_numerals real_le_add_order] addDs 
   3.115 -    [real_le_trans],simpset() 
   3.116 +    [real_le_trans], simpset() 
   3.117      addsimps [abs_ge_zero,rename_numerals real_zero_less_one,abs_eqI1]));
   3.118  by (subgoal_tac "k < 0" 1);
   3.119  by (rtac (real_not_leE RSN (2,real_le_less_trans)) 2);
   3.120 @@ -874,7 +875,7 @@
   3.121      (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
   3.122  by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
   3.123  by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
   3.124 -        FreeUltrafilterNat_Nat_set],simpset()));
   3.125 +        FreeUltrafilterNat_Nat_set], simpset()));
   3.126  qed "Cauchy_NSCauchy";
   3.127  
   3.128  (*-----------------------------------------------
   3.129 @@ -1052,7 +1053,7 @@
   3.130      [NSBseq_def,NSCauchy_def]));
   3.131  by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
   3.132  by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
   3.133 -by (auto_tac (claset() addSDs [st_part_Ex],simpset() 
   3.134 +by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
   3.135                addsimps [SReal_iff]));
   3.136  by (blast_tac (claset() addIs [inf_close_trans3]) 1);
   3.137  qed "NSCauchy_NSconvergent_iff";
   3.138 @@ -1077,7 +1078,7 @@
   3.139  by (dres_inst_tac [("x","whn")] spec 1);
   3.140  by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
   3.141  by (auto_tac (claset() addIs 
   3.142 -    [hypreal_of_real_le_add_Infininitesimal_cancel2],simpset()));
   3.143 +    [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
   3.144  qed "NSLIMSEQ_le";
   3.145  
   3.146  (* standard version *)
   3.147 @@ -1188,7 +1189,7 @@
   3.148   ---------------------------------------*)
   3.149  Goalw [NSLIMSEQ_def] 
   3.150         "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
   3.151 -by (auto_tac (claset() addIs [inf_close_hrabs],simpset() 
   3.152 +by (auto_tac (claset() addIs [inf_close_hrabs], simpset() 
   3.153      addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
   3.154  qed "NSLIMSEQ_imp_rabs";
   3.155  
   3.156 @@ -1214,7 +1215,7 @@
   3.157  by (forw_inst_tac [("x","f n")] (rename_numerals real_rinv_gt_zero) 1);
   3.158  by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
   3.159  by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
   3.160 -by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1],simpset()));
   3.161 +by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1], simpset()));
   3.162  qed "LIMSEQ_rinv_zero";
   3.163  
   3.164  Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
   3.165 @@ -1232,7 +1233,7 @@
   3.166  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
   3.167  by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
   3.168  by (dtac (real_of_posnat_less_iff RS iffD2) 1);
   3.169 -by (auto_tac (claset() addEs [real_less_trans],simpset()));
   3.170 +by (auto_tac (claset() addEs [real_less_trans], simpset()));
   3.171  qed "LIMSEQ_rinv_real_of_posnat";
   3.172  
   3.173  Goal "(%n. rinv(real_of_posnat n)) ----NS> #0";
   3.174 @@ -1304,7 +1305,7 @@
   3.175        "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
   3.176  by (res_inst_tac [("x","#1")] exI 1);
   3.177  by (auto_tac (claset() addDs [conjI RS realpow_le2] 
   3.178 -    addIs [real_less_imp_le],simpset() addsimps 
   3.179 +    addIs [real_less_imp_le], simpset() addsimps 
   3.180      [real_zero_less_one,abs_eqI1,realpow_abs RS sym] ));
   3.181  qed "Bseq_realpow";
   3.182  
   3.183 @@ -1334,9 +1335,9 @@
   3.184  by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
   3.185  by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
   3.186  by (dtac inf_close_trans3 1 THEN assume_tac 1);
   3.187 -by (auto_tac (claset() addSDs [rename_numerals (real_not_refl2 RS 
   3.188 -    real_mult_eq_self_zero2)],simpset() addsimps 
   3.189 -    [hypreal_of_real_mult RS sym]));
   3.190 +by (auto_tac (claset() addSDs [rename_numerals 
   3.191 +                                (real_not_refl2 RS real_mult_eq_self_zero2)], 
   3.192 +    simpset() addsimps [hypreal_of_real_mult RS sym]));
   3.193  qed "NSLIMSEQ_realpow_zero";
   3.194  
   3.195  (*---------------  standard version ---------------*)
     4.1 --- a/src/HOL/Real/Hyperreal/Series.ML	Thu Nov 30 20:18:00 2000 +0100
     4.2 +++ b/src/HOL/Real/Hyperreal/Series.ML	Fri Dec 01 11:02:55 2000 +0100
     4.3 @@ -43,7 +43,7 @@
     4.4  Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f";
     4.5  by (induct_tac "p" 1);
     4.6  by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
     4.7 -    leI] addDs [le_anti_sym],simpset()));
     4.8 +    leI] addDs [le_anti_sym], simpset()));
     4.9  qed_spec_mp "sumr_split_add";
    4.10  
    4.11  Goal "!!n. n < p ==> sumr 0 p f + \
    4.12 @@ -55,7 +55,7 @@
    4.13  Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))";
    4.14  by (induct_tac "n" 1);
    4.15  by (auto_tac (claset() addIs [(abs_triangle_ineq 
    4.16 -    RS real_le_trans),real_add_le_mono1],simpset()));
    4.17 +    RS real_le_trans),real_add_le_mono1], simpset()));
    4.18  qed "sumr_rabs";
    4.19  
    4.20  Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
    4.21 @@ -83,7 +83,7 @@
    4.22  
    4.23  Goal "n < m --> sumr m n f = #0";
    4.24  by (induct_tac "n" 1);
    4.25 -by (auto_tac (claset() addDs [less_imp_le],simpset()));
    4.26 +by (auto_tac (claset() addDs [less_imp_le], simpset()));
    4.27  qed_spec_mp "sumr_less_bounds_zero";
    4.28  Addsimps [sumr_less_bounds_zero];
    4.29  
    4.30 @@ -97,7 +97,7 @@
    4.31  context NatArith.thy;
    4.32  
    4.33  Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
    4.34 -by (auto_tac (claset() addSDs [not_leE],simpset()));
    4.35 +by (auto_tac (claset() addSDs [not_leE], simpset()));
    4.36  qed "lemma_not_Suc_add";
    4.37  
    4.38  context thy;
    4.39 @@ -120,7 +120,7 @@
    4.40  Addsimps [sumr_minus_one_realpow_zero2];
    4.41  
    4.42  Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
    4.43 -by (dtac less_eq_Suc_add 1);
    4.44 +by (dtac less_imp_Suc_add 1);
    4.45  by (Auto_tac);
    4.46  val Suc_diff_n = result();
    4.47  
    4.48 @@ -185,13 +185,13 @@
    4.49  Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f";
    4.50  by (induct_tac "n" 1);
    4.51  by (auto_tac (claset() addIs [rename_numerals real_le_add_order] 
    4.52 -    addDs [leI],simpset()));
    4.53 +    addDs [leI], simpset()));
    4.54  qed_spec_mp "sumr_ge_zero2";
    4.55  
    4.56  Goal "#0 <= sumr m n (%n. abs (f n))";
    4.57  by (induct_tac "n" 1);
    4.58  by (auto_tac (claset() addSIs [rename_numerals real_le_add_order,
    4.59 -    abs_ge_zero],simpset()));
    4.60 +    abs_ge_zero], simpset()));
    4.61  qed "sumr_rabs_ge_zero";
    4.62  Addsimps [sumr_rabs_ge_zero];
    4.63  AddSIs [sumr_rabs_ge_zero]; 
    4.64 @@ -350,12 +350,12 @@
    4.65  
    4.66  Goal "[| summable f; summable g |]  \
    4.67  \     ==> suminf f - suminf g  = suminf(%n. f n - g n)";
    4.68 -by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums],simpset()));
    4.69 +by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset()));
    4.70  qed "suminf_diff";
    4.71  
    4.72  goalw Series.thy [sums_def] 
    4.73         "!!x. x sums x0 ==> (%n. - x n) sums - x0";
    4.74 -by (auto_tac (claset() addSIs [LIMSEQ_minus],simpset() addsimps [sumr_minus]));
    4.75 +by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus]));
    4.76  qed "sums_minus";
    4.77  
    4.78  Goal "[|summable f; 0 < k |] \
    4.79 @@ -365,7 +365,7 @@
    4.80  by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); 
    4.81  by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); 
    4.82  by (dres_inst_tac [("x","n*k")] spec 1); 
    4.83 -by (auto_tac (claset() addSDs [not_leE],simpset()));
    4.84 +by (auto_tac (claset() addSDs [not_leE], simpset()));
    4.85  by (dres_inst_tac [("j","no")] less_le_trans 1);
    4.86  by (Auto_tac);
    4.87  qed "sums_group";
    4.88 @@ -416,7 +416,7 @@
    4.89  by (etac LIMSEQ_le 1 THEN Step_tac 1);
    4.90  by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
    4.91  by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
    4.92 -by (auto_tac (claset() addIs [sumr_le],simpset()));
    4.93 +by (auto_tac (claset() addIs [sumr_le], simpset()));
    4.94  qed "series_pos_le";
    4.95  
    4.96  Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \
    4.97 @@ -524,15 +524,15 @@
    4.98  Goal "[|ALL n. f n <= g n; summable f; summable g |] \
    4.99  \     ==> suminf f <= suminf g";
   4.100  by (REPEAT(dtac summable_sums 1));
   4.101 -by (auto_tac (claset() addSIs [LIMSEQ_le],simpset() addsimps [sums_def]));
   4.102 +by (auto_tac (claset() addSIs [LIMSEQ_le], simpset() addsimps [sums_def]));
   4.103  by (rtac exI 1);
   4.104 -by (auto_tac (claset() addSIs [sumr_le2],simpset()));
   4.105 +by (auto_tac (claset() addSIs [sumr_le2], simpset()));
   4.106  qed "summable_le";
   4.107  
   4.108  Goal "[|ALL n. abs(f n) <= g n; summable g |] \
   4.109  \     ==> summable f & suminf f <= suminf g";
   4.110  by (auto_tac (claset() addIs [summable_comparison_test]
   4.111 -    addSIs [summable_le],simpset()));
   4.112 +    addSIs [summable_le], simpset()));
   4.113  by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff]));
   4.114  qed "summable_le2";
   4.115  
   4.116 @@ -545,7 +545,7 @@
   4.117  by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac);
   4.118  by (dtac spec 1 THEN Auto_tac);
   4.119  by (res_inst_tac [("j","sumr m n (%n. abs(f n))")] real_le_less_trans 1);
   4.120 -by (auto_tac (claset() addIs [sumr_rabs],simpset()));
   4.121 +by (auto_tac (claset() addIs [sumr_rabs], simpset()));
   4.122  qed "summable_rabs_cancel";
   4.123  
   4.124  (*-------------------------------------------------------------------
   4.125 @@ -553,7 +553,7 @@
   4.126   -------------------------------------------------------------------*)
   4.127  Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))";
   4.128  by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel,
   4.129 -    summable_sumr_LIMSEQ_suminf,sumr_rabs],simpset()));
   4.130 +    summable_sumr_LIMSEQ_suminf,sumr_rabs], simpset()));
   4.131  qed "summable_rabs";
   4.132  
   4.133  (*-------------------------------------------------------------------
   4.134 @@ -585,7 +585,7 @@
   4.135  
   4.136  Goal "(k::nat) <= l ==> (EX n. l = k + n)";
   4.137  by (dtac le_imp_less_or_eq 1);
   4.138 -by (auto_tac (claset() addDs [less_eq_Suc_add],simpset()));
   4.139 +by (auto_tac (claset() addDs [less_imp_Suc_add], simpset()));
   4.140  qed "le_Suc_ex";
   4.141  
   4.142  Goal "((k::nat) <= l) = (EX n. l = k + n)";
   4.143 @@ -613,7 +613,7 @@
   4.144      simpset() addsimps [summable_def, CLAIM_SIMP 
   4.145      "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
   4.146  by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1);
   4.147 -by (auto_tac (claset() addSIs [sums_mult,geometric_sums],simpset() addsimps 
   4.148 +by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps 
   4.149      [abs_eqI2]));
   4.150  qed "ratio_test";
   4.151  
   4.152 @@ -625,7 +625,7 @@
   4.153  Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
   4.154  \     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
   4.155  by (induct_tac "n" 1);
   4.156 -by (auto_tac (claset() addIs [DERIV_add],simpset()));
   4.157 +by (auto_tac (claset() addIs [DERIV_add], simpset()));
   4.158  qed "DERIV_sumr";
   4.159  
   4.160  
     5.1 --- a/src/HOL/ex/Primrec.ML	Thu Nov 30 20:18:00 2000 +0100
     5.2 +++ b/src/HOL/ex/Primrec.ML	Fri Dec 01 11:02:55 2000 +0100
     5.3 @@ -125,7 +125,7 @@
     5.4  val lemma = result();
     5.5  
     5.6  Goal "i<j ==> ack(i,k) < ack(j,k)";
     5.7 -by (dtac less_eq_Suc_add 1);
     5.8 +by (dtac less_imp_Suc_add 1);
     5.9  by (blast_tac (claset() addSIs [lemma]) 1);
    5.10  qed "ack_less_mono1";
    5.11