# HG changeset patch
# User huffman
# Date 1178762816 -7200
# Node ID bb8a928a6bfa7451c2c7bda9757627fa375c9b77
# Parent  681700e1d6932e648014d1bf52609edafabfbe3d
fix proofs

diff -r 681700e1d693 -r bb8a928a6bfa src/HOL/Hyperreal/Transcendental.thy
--- 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