src/HOL/Transcendental.thy

--- a/src/HOL/Transcendental.thy	Fri Aug 19 16:55:43 2011 -0700
+++ b/src/HOL/Transcendental.thy	Fri Aug 19 17:59:19 2011 -0700
@@ -1159,9 +1159,6 @@
 lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
   by simp
 
-lemma exp_ln_eq: "exp u = x ==> ln x = u"
-  by (rule ln_unique) (* TODO: delete *)
-
 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
   apply (subgoal_tac "isCont ln (exp (ln x))", simp)
   apply (rule isCont_inverse_function [where f=exp], simp_all)