changeset 44316 | 84b6f7a6cea4 |
parent 37887 | 2ae085b07f2f |
child 53077 | a1b3784f8129 |
--- 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)