src/HOL/Library/Poly_Deriv.thy
changeset 30273 ecd6f0ca62ea
parent 29985 57975b45ab70
child 31881 eba74a5790d2
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -139,7 +139,7 @@
     1.4    "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
     1.5      smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
     1.6  apply (simp only: pderiv_mult pderiv_power_Suc)
     1.7 -apply (simp del: power_poly_Suc of_nat_Suc add: pderiv_pCons)
     1.8 +apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
     1.9  done
    1.10  
    1.11  lemma dvd_add_cancel1: