changeset 30273 | ecd6f0ca62ea |
parent 29986 | 6b1ccda8bf19 |
child 30663 | 0b6aff7451b2 |
--- a/src/HOL/Library/FrechetDeriv.thy Thu Mar 05 00:16:28 2009 +0100 +++ b/src/HOL/Library/FrechetDeriv.thy Wed Mar 04 17:12:23 2009 -0800 @@ -397,7 +397,7 @@ shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)" apply (cases n) apply (simp add: FDERIV_const) - apply (simp add: FDERIV_power_Suc) + apply (simp add: FDERIV_power_Suc del: power_Suc) done