src/HOL/Series.thy
changeset 56217 dc429a5b13c4
parent 56213 e5720d3c18f0
child 56369 2704ca85be98
     1.1 --- a/src/HOL/Series.thy	Wed Mar 19 14:55:47 2014 +0000
     1.2 +++ b/src/HOL/Series.thy	Wed Mar 19 17:06:02 2014 +0000
     1.3 @@ -461,6 +461,10 @@
     1.4    apply (auto intro: setsum_mono simp add: abs_less_iff)
     1.5    done
     1.6  
     1.7 +(*A better argument order*)
     1.8 +lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
     1.9 +by (rule summable_comparison_test) auto
    1.10 +
    1.11  subsection {* The Ratio Test*}
    1.12  
    1.13  lemma summable_ratio_test: