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/Poly_Deriv.thy
changeset 30273 ecd6f0ca62ea
parent 29985 57975b45ab70
child 31881 eba74a5790d2 
--- a/src/HOL/Library/Poly_Deriv.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -139,7 +139,7 @@
   "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
     smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
 apply (simp only: pderiv_mult pderiv_power_Suc)
-apply (simp del: power_poly_Suc of_nat_Suc add: pderiv_pCons)
+apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
 done
 
 lemma dvd_add_cancel1:
isabelle