diff -r 036c46df9576 -r 74bc935273ea src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Wed Aug 03 14:48:36 2005 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Wed Aug 03 14:48:42 2005 +0200
@@ -167,7 +167,7 @@
     done
   also have "... <= (1 + x + x^2) / (1 + x^2)"
     apply (rule divide_left_mono)
-    apply auto
+    apply (auto simp add: exp_ge_add_one_self_aux)
     apply (rule add_nonneg_nonneg)
     apply (insert prems, auto)
     apply (rule mult_pos_pos)
@@ -295,9 +295,9 @@
     by (rule order_trans)
 qed
 
-lemma exp_ge_add_one_self2: "1 + x <= exp x"
+lemma exp_ge_add_one_self [simp]: "1 + x <= exp x"
   apply (case_tac "0 <= x")
-  apply (erule exp_ge_add_one_self)
+  apply (erule exp_ge_add_one_self_aux)
   apply (case_tac "x <= -1")
   apply (subgoal_tac "1 + x <= 0")
   apply (erule order_trans)
@@ -320,7 +320,6 @@
   apply (erule ssubst)back
   apply (subst ln_le_cancel_iff)
   apply auto
-  apply (rule exp_ge_add_one_self2)
 done
 
 lemma abs_ln_one_plus_x_minus_x_bound_nonneg: