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:
```