src/HOL/Series.thy
changeset 58729 e8ecc79aee43
parent 57418 6ab1c7cb0b8d
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Series.thy	Mon Oct 20 23:17:28 2014 +0200
     1.2 +++ b/src/HOL/Series.thy	Mon Oct 20 18:33:14 2014 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4    by (simp add: suminf_def sums_def lim_def)
     1.5  
     1.6  lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
     1.7 -  unfolding sums_def by (simp add: tendsto_const)
     1.8 +  unfolding sums_def by simp
     1.9  
    1.10  lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    1.11    by (rule sums_zero [THEN sums_summable])
    1.12 @@ -84,7 +84,7 @@
    1.13    note eq = this
    1.14    show ?thesis unfolding sums_def
    1.15      by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
    1.16 -       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
    1.17 +       (simp add: eq atLeast0LessThan del: add_Suc_right)
    1.18  qed
    1.19  
    1.20  lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
    1.21 @@ -232,7 +232,7 @@
    1.22      with tendsto_add[OF this tendsto_const, of "- f 0"]
    1.23      show "(\<lambda>i. f (Suc i)) sums s"
    1.24        by (simp add: sums_def)
    1.25 -  qed (auto intro: tendsto_add tendsto_const simp: sums_def)
    1.26 +  qed (auto intro: tendsto_add simp: sums_def)
    1.27    finally show ?thesis ..
    1.28  qed
    1.29