# HG changeset patch
# User avigad
# Date 1123073336 -7200
# Node ID 50e1d2be7e67d208f432948c8a2acee3cfe2d96d
# Parent  ad5ceb90877d3854315afae91d5a4d2909a38c88
changes from renaming of exp_ge_add_one_self

diff -r ad5ceb90877d -r 50e1d2be7e67 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Aug 03 14:48:50 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Aug 03 14:48:56 2005 +0200
@@ -312,6 +312,7 @@
 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
 apply (cases x)
 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
+apply (erule exp_ge_add_one_self_aux)
 done
 
 (* exp (oo) is infinite *)