src/HOL/NSA/HTranscendental.thy
changeset 44316 84b6f7a6cea4
parent 37887 2ae085b07f2f
child 53077 a1b3784f8129
     1.1 --- a/src/HOL/NSA/HTranscendental.thy	Fri Aug 19 16:55:43 2011 -0700
     1.2 +++ b/src/HOL/NSA/HTranscendental.thy	Fri Aug 19 17:59:19 2011 -0700
     1.3 @@ -311,7 +311,7 @@
     1.4  by transfer (rule exp_ln_iff)
     1.5  
     1.6  lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
     1.7 -by transfer (rule exp_ln_eq)
     1.8 +by transfer (rule ln_unique)
     1.9  
    1.10  lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
    1.11  by transfer (rule ln_less_self)