diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Series.thy --- a/src/HOL/Series.thy Wed Mar 19 14:55:47 2014 +0000 +++ b/src/HOL/Series.thy Wed Mar 19 17:06:02 2014 +0000 @@ -461,6 +461,10 @@ apply (auto intro: setsum_mono simp add: abs_less_iff) done +(*A better argument order*) +lemma summable_comparison_test': "summable g \ (\n. n \ N \ norm(f n) \ g n) \ summable f" +by (rule summable_comparison_test) auto + subsection {* The Ratio Test*} lemma summable_ratio_test: