src/HOL/Hyperreal/Series.thy
changeset 22998 97e1f9c2cc46
parent 22959 07a7c2900877
child 23084 bc000fc64fce
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Thu May 17 19:49:40 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Thu May 17 21:51:32 2007 +0200
     1.3 @@ -422,7 +422,7 @@
     1.4  apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
     1.5  apply (rule norm_setsum)
     1.6  apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
     1.7 -apply (auto intro: setsum_mono simp add: abs_interval_iff)
     1.8 +apply (auto intro: setsum_mono simp add: abs_less_iff)
     1.9  done
    1.10  
    1.11  lemma summable_norm_comparison_test:
    1.12 @@ -456,7 +456,7 @@
    1.13    shows "\<lbrakk>\<forall>n. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f \<and> suminf f \<le> suminf g"
    1.14  apply (subgoal_tac "summable f")
    1.15  apply (auto intro!: summable_le)
    1.16 -apply (simp add: abs_le_interval_iff)
    1.17 +apply (simp add: abs_le_iff)
    1.18  apply (rule_tac g="g" in summable_comparison_test, simp_all)
    1.19  done
    1.20