Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/FrechetDeriv.thy
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
isabelle