remove redundant lemma exp_ln_eq in favor of ln_unique

--- a/src/HOL/NSA/HTranscendental.thy	Fri Aug 19 16:55:43 2011 -0700
+++ b/src/HOL/NSA/HTranscendental.thy	Fri Aug 19 17:59:19 2011 -0700
@@ -311,7 +311,7 @@
 by transfer (rule exp_ln_iff)
 
 lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
-by transfer (rule exp_ln_eq)
+by transfer (rule ln_unique)
 
 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
 by transfer (rule ln_less_self)

--- 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)