author | avigad |
Wed, 03 Aug 2005 14:48:56 +0200 | |
changeset 17015 | 50e1d2be7e67 |
parent 17014 | ad5ceb90877d |
child 17016 | 73c74cb1d744 |
--- 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 *)