# HG changeset patch
# User hoelzl
# Date 1306870429 -7200
# Node ID 9f8766a8ebe09d5d026030d167ef00c82f796ea1
# Parent  048c7eea1a719cf061c55ac90149e48d14700678
use divide instead of inverse for the derivative of ln

diff -r 048c7eea1a71 -r 9f8766a8ebe0 src/HOL/Transcendental.thy
--- 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]