| changeset 56381 | 0556204bc230 |
| parent 56217 | dc429a5b13c4 |
| child 56383 | 8e7052e9fda4 |
--- a/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 17:56:08 2014 +0200 @@ -102,7 +102,7 @@ by (rule DERIV_cong, rule DERIV_add, auto) lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" - by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons) + by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) text{* Consequences of the derivative theorem above*}