Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changes from renaming of exp_ge_add_one_self
authoravigad
Wed, 03 Aug 2005 14:48:56 +0200
changeset 17015 50e1d2be7e67
parent 17014 ad5ceb90877d
child 17016 73c74cb1d744
changes from renaming of exp_ge_add_one_self
src/HOL/Hyperreal/HTranscendental.thy file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle