src/HOL/Library/Poly_Deriv.thy
changeset 31881 eba74a5790d2
parent 30273 ecd6f0ca62ea
child 35050 9f841f20dca6
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:16:22 2009 +0200
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:21:55 2009 +0200
     1.3 @@ -85,13 +85,7 @@
     1.4  by (rule lemma_DERIV_subst, rule DERIV_add, auto)
     1.5  
     1.6  lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
     1.7 -apply (induct p)
     1.8 -apply simp
     1.9 -apply (simp add: pderiv_pCons)
    1.10 -apply (rule lemma_DERIV_subst)
    1.11 -apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
    1.12 -apply simp
    1.13 -done
    1.14 +  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
    1.15  
    1.16  text{* Consequences of the derivative theorem above*}
    1.17