diff -r 340738057c8c -r a6479cb85944 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Transcendental.thy	Tue Feb 23 15:47:39 2016 +0000
@@ -472,10 +472,6 @@
 lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
   by (simp add: diffs_def)
 
-lemma sums_Suc_imp:
-  "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
-  using sums_Suc_iff[of f] by simp
-
 lemma diffs_equiv:
   fixes x :: "'a::{real_normed_vector, ring_1}"
   shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>