src/HOL/Transcendental.thy
changeset 45915 0e5a87b772f9
parent 45309 5885ec8eb6b0
child 46240 933f35c4e126
     1.1 --- a/src/HOL/Transcendental.thy	Sun Dec 18 14:28:14 2011 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Thu Dec 15 17:21:29 2011 +0100
     1.3 @@ -1166,6 +1166,10 @@
     1.4    apply (rule isCont_inverse_function [where f=exp], simp_all)
     1.5    done
     1.6  
     1.7 +lemma tendsto_ln [tendsto_intros]:
     1.8 +  "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
     1.9 +  by (rule isCont_tendsto_compose [OF isCont_ln])
    1.10 +
    1.11  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
    1.12    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
    1.13    apply (erule DERIV_cong [OF DERIV_exp exp_ln])