src/HOL/Transcendental.thy
changeset 44316 84b6f7a6cea4
parent 44311 42c5cbf68052
child 44317 b7e9fa025f15
     1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 16:55:43 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 17:59:19 2011 -0700
     1.3 @@ -1159,9 +1159,6 @@
     1.4  lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
     1.5    by simp
     1.6  
     1.7 -lemma exp_ln_eq: "exp u = x ==> ln x = u"
     1.8 -  by (rule ln_unique) (* TODO: delete *)
     1.9 -
    1.10  lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
    1.11    apply (subgoal_tac "isCont ln (exp (ln x))", simp)
    1.12    apply (rule isCont_inverse_function [where f=exp], simp_all)