# HG changeset patch
# User avigad
# Date 1123073322 -7200
# Node ID 74bc935273ea53a49f35377d1182d6e3e31bb690
# Parent  036c46df9576a2ff0288ccf3f52ee7f84dcbce8c
renamed exp_ge_add_one_self2 to exp_ge_add_one_self

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: