src/HOL/Series.thy

 lemma sums_split_initial_segment:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   apply (unfold sums_def)
   apply (simp add: sumr_offset)
-  apply (rule LIMSEQ_diff_const)
+  apply (rule tendsto_diff [OF _ tendsto_const])
   apply (rule LIMSEQ_ignore_initial_segment)
   apply assumption
 done
 
 lemma summable_ignore_initial_segment:

   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   assumes sumSuc: "(\<lambda> n. f (Suc n)) sums l" shows "f sums (l + f 0)"
 proof -
   from sumSuc[unfolded sums_def]
   have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
-  from LIMSEQ_add_const[OF this, where b="f 0"]
+  from tendsto_add[OF this tendsto_const, where b="f 0"]
   have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
   thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
 qed
 
 lemma series_zero:

  apply clarify
  apply(erule_tac x = "n - Suc 0" in allE)
  apply (simp add:diff_Suc split:nat.splits)
  apply (blast intro: norm_ratiotest_lemma)
 apply (rule_tac x = "Suc N" in exI, clarify)
-apply(simp cong:setsum_ivl_cong)
+apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
 done
 
 lemma ratio_test:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   shows "\<lbrakk>c < 1; \<forall>n\<ge>N. norm (f (Suc n)) \<le> c * norm (f n)\<rbrakk> \<Longrightarrow> summable f"