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