1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Sep 01 19:16:40 2008 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Sep 01 19:17:04 2008 +0200
     1.3 @@ -669,13 +669,9 @@
     1.4  lemma exp_zero [simp]: "exp 0 = 1"
     1.5  unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
     1.6  
     1.7 -lemma setsum_head2:
     1.8 -  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
     1.9 -by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
    1.10 -
    1.11  lemma setsum_cl_ivl_Suc2:
    1.12    "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
    1.13 -by (simp add: setsum_head2 setsum_shift_bounds_cl_Suc_ivl
    1.14 +by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
    1.15           del: setsum_cl_ivl_Suc)
    1.16  
    1.17  lemma exp_series_add: