--- a/src/HOL/Library/Poly_Deriv.thy Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy Tue Jun 30 18:21:55 2009 +0200
@@ -85,13 +85,7 @@
by (rule lemma_DERIV_subst, rule DERIV_add, auto)
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+ by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
text{* Consequences of the derivative theorem above*}