Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use divide instead of inverse for the derivative of ln
authorhoelzl
Tue, 31 May 2011 21:33:49 +0200
changeset 43335 9f8766a8ebe0
parent 43319 048c7eea1a71
child 43336 05aa7380f7fc
use divide instead of inverse for the derivative of ln
src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Transcendental.thy	Thu Jun 09 10:43:42 2011 +0200
+++ b/src/HOL/Transcendental.thy	Tue May 31 21:33:49 2011 +0200
@@ -1366,7 +1366,7 @@
 
 declare
   DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
-  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
isabelle