# HG changeset patch
# User huffman
# Date 1313801959 25200
# Node ID 84b6f7a6cea4037e832351f4041083ac9aef9c3a
# Parent  349842366154ad35e99cd46a30f2154180427418
remove redundant lemma exp_ln_eq in favor of ln_unique

diff -r 349842366154 -r 84b6f7a6cea4 src/HOL/NSA/HTranscendental.thy
--- 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)
diff -r 349842366154 -r 84b6f7a6cea4 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)