--- 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: