use divide instead of inverse for the derivative of ln
authorhoelzl
Tue May 31 21:33:49 2011 +0200 (2011-05-31)
changeset 433359f8766a8ebe0
parent 43319 048c7eea1a71
child 43336 05aa7380f7fc
use divide instead of inverse for the derivative of ln
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Thu Jun 09 10:43:42 2011 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Tue May 31 21:33:49 2011 +0200
     1.3 @@ -1366,7 +1366,7 @@
     1.4  
     1.5  declare
     1.6    DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
     1.7 -  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
     1.8 +  DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
     1.9    DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.10    DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.11