equal
deleted
inserted
replaced
230 |
230 |
231 lemma NSsummable_rabs_comparison_test: |
231 lemma NSsummable_rabs_comparison_test: |
232 "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] |
232 "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] |
233 ==> NSsummable (%k. abs (f k))" |
233 ==> NSsummable (%k. abs (f k))" |
234 apply (rule NSsummable_comparison_test) |
234 apply (rule NSsummable_comparison_test) |
235 apply (auto simp add: abs_idempotent) |
235 apply (auto) |
236 done |
236 done |
237 |
237 |
238 ML |
238 ML |
239 {* |
239 {* |
240 val sumhr = thm "sumhr"; |
240 val sumhr = thm "sumhr"; |