changeset 56181 | 2aa0b19e74f3 |
parent 52380 | 3cc46b8cca5e |
child 56217 | dc429a5b13c4 |
--- a/src/HOL/Library/Poly_Deriv.thy Mon Mar 17 18:06:59 2014 +0100 +++ b/src/HOL/Library/Poly_Deriv.thy Mon Mar 17 19:12:52 2014 +0100 @@ -106,8 +106,8 @@ text{* Consequences of the derivative theorem above*} -lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (x::real)" -apply (simp add: differentiable_def) +lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)" +apply (simp add: real_differentiable_def) apply (blast intro: poly_DERIV) done