src/HOL/MacLaurin.thy
changeset 57514 bdc2c6b40bf2
parent 57492 74bf65a1910a
child 58410 6d46ad54a2ab
     1.1 --- a/src/HOL/MacLaurin.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -574,7 +574,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_ac divide_inverse power_abs [symmetric] abs_mult)
     1.8 +                simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult)
     1.9      done
    1.10  qed
    1.11