src/HOL/MacLaurin.thy
changeset 56536 aefb4a8da31f
parent 56381 0556204bc230
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/MacLaurin.thy	Fri Apr 11 12:43:22 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Fri Apr 11 13:36:57 2014 +0200
     1.3 @@ -575,8 +575,7 @@
     1.4      apply (rule setsum_cong[OF refl])
     1.5      apply (subst diff_m_0, simp)
     1.6      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
     1.7 -                simp add: est mult_nonneg_nonneg mult_ac divide_inverse
     1.8 -                          power_abs [symmetric] abs_mult)
     1.9 +                simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
    1.10      done
    1.11  qed
    1.12