src/HOL/Series.thy
changeset 44727 d45acd50a894
parent 44726 8478eab380e9
child 46904 f30e941b4512
     1.1 --- a/src/HOL/Series.thy	Mon Sep 05 16:07:40 2011 -0700
     1.2 +++ b/src/HOL/Series.thy	Mon Sep 05 16:26:57 2011 -0700
     1.3 @@ -304,8 +304,7 @@
     1.4  
     1.5  lemma sums_group:
     1.6    fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
     1.7 -  shows "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
     1.8 -apply (drule summable_sums)
     1.9 +  shows "\<lbrakk>f sums s; 0 < k\<rbrakk> \<Longrightarrow> (\<lambda>n. setsum f {n*k..<n*k+k}) sums s"
    1.10  apply (simp only: sums_def sumr_group)
    1.11  apply (unfold LIMSEQ_iff, safe)
    1.12  apply (drule_tac x="r" in spec, safe)
    1.13 @@ -380,7 +379,7 @@
    1.14  apply assumption
    1.15  apply simp
    1.16  apply (drule_tac k="k" in summable_ignore_initial_segment)
    1.17 -apply (drule_tac k="Suc (Suc 0)" in sums_group, simp)
    1.18 +apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
    1.19  apply simp
    1.20  apply (frule sums_unique)
    1.21  apply (drule sums_summable)