| changeset 57514 | bdc2c6b40bf2 |
| parent 57492 | 74bf65a1910a |
| child 58410 | 6d46ad54a2ab |
--- a/src/HOL/MacLaurin.thy Sat Jul 05 10:09:01 2014 +0200 +++ b/src/HOL/MacLaurin.thy Sat Jul 05 11:01:53 2014 +0200 @@ -574,7 +574,7 @@ apply (rule setsum.cong[OF refl]) apply (subst diff_m_0, simp) apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono - simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult) + simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult) done qed