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 \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
+by (rule summable_comparison_test) auto
+
 subsection {* The Ratio Test*}
 
 lemma summable_ratio_test: