src/HOL/Transcendental.thy
changeset 43335 9f8766a8ebe0
parent 41970 47d6e13d1710
child 44282 f0de18b62d63
     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