src/HOL/Deriv.thy
changeset 29472 a63a2e46cec9
parent 29470 1851088a1f87
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/Deriv.thy	Tue Jan 13 07:40:05 2009 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Tue Jan 13 08:19:14 2009 -0800
     1.3 @@ -1475,7 +1475,7 @@
     1.4  apply (subst power_Suc)
     1.5  apply (subst pderiv_mult)
     1.6  apply (erule ssubst)
     1.7 -apply (simp add: mult_smult_right mult_smult_left smult_add_left ring_simps)
     1.8 +apply (simp add: smult_add_left ring_simps)
     1.9  done
    1.10  
    1.11  lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"