--- a/src/HOL/Hyperreal/Transcendental.thy Thu May 10 03:11:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu May 10 04:06:56 2007 +0200
@@ -845,7 +845,7 @@
proof -
have "0 < x" using x by arith
hence "exp 0 \<le> exp (ln x)"
- by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
+ by (simp add: x)
thus ?thesis by (simp only: exp_le_cancel_iff)
qed
@@ -868,8 +868,7 @@
assumes x: "1 < x" shows "0 < ln x"
proof -
have "0 < x" using x by arith
- hence "exp 0 < exp (ln x)"
- by (simp add: x exp_ln_iff [symmetric] del: exp_ln_iff)
+ hence "exp 0 < exp (ln x)" by (simp add: x)
thus ?thesis by (simp only: exp_less_cancel_iff)
qed