src/HOL/Series.thy
changeset 51477 2990382dc066
parent 50999 3de230ed0547
child 51526 155263089e7b
     1.1 --- a/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -373,16 +373,13 @@
     1.4    have "convergent (\<lambda>n. setsum f {0..<n})"
     1.5      proof (rule Bseq_mono_convergent)
     1.6        show "Bseq (\<lambda>n. setsum f {0..<n})"
     1.7 -        by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
     1.8 -           (auto simp add: le pos)
     1.9 +        by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
    1.10      next
    1.11        show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
    1.12          by (auto intro: setsum_mono2 pos)
    1.13      qed
    1.14 -  then obtain L where "(%n. setsum f {0..<n}) ----> L"
    1.15 -    by (blast dest: convergentD)
    1.16    thus ?thesis
    1.17 -    by (force simp add: summable_def sums_def)
    1.18 +    by (force simp add: summable_def sums_def convergent_def)
    1.19  qed
    1.20  
    1.21  lemma series_pos_le: