| changeset 56217 | dc429a5b13c4 |
| parent 56181 | 2aa0b19e74f3 |
| child 56381 | 0556204bc230 |
--- a/src/HOL/Library/Poly_Deriv.thy Wed Mar 19 14:55:47 2014 +0000 +++ b/src/HOL/Library/Poly_Deriv.thy Wed Mar 19 17:06:02 2014 +0000 @@ -128,7 +128,7 @@ \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" apply (drule_tac f = "poly p" in MVT, auto) apply (rule_tac x = z in exI) -apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique]) +apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) done text{*Lemmas for Derivatives*}