--- a/src/HOL/Log.thy Sun Dec 18 14:28:14 2011 +0100
+++ b/src/HOL/Log.thy Thu Dec 15 17:21:29 2011 +0100
@@ -285,6 +285,10 @@
finally show ?thesis .
qed
+lemma tendsto_powr [tendsto_intros]:
+ "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
+ unfolding powr_def by (intro tendsto_intros)
+
(* FIXME: generalize by replacing d by with g x and g ---> d? *)
lemma tendsto_zero_powrI:
assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
--- a/src/HOL/Transcendental.thy Sun Dec 18 14:28:14 2011 +0100
+++ b/src/HOL/Transcendental.thy Thu Dec 15 17:21:29 2011 +0100
@@ -1166,6 +1166,10 @@
apply (rule isCont_inverse_function [where f=exp], simp_all)
done
+lemma tendsto_ln [tendsto_intros]:
+ "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
+ by (rule isCont_tendsto_compose [OF isCont_ln])
+
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
apply (erule DERIV_cong [OF DERIV_exp exp_ln])