equal
deleted
inserted
replaced
360 by (transfer, rule ln_inverse) |
360 by (transfer, rule ln_inverse) |
361 |
361 |
362 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite" |
362 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite" |
363 apply (cases x) |
363 apply (cases x) |
364 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff) |
364 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff) |
365 apply (rule bexI [OF _ Rep_star_star_n], auto) |
|
366 apply (rule_tac x = "exp u" in exI) |
365 apply (rule_tac x = "exp u" in exI) |
367 apply ultra |
366 apply ultra |
368 done |
367 done |
369 |
368 |
370 lemma starfun_exp_add_HFinite_Infinitesimal_approx: |
369 lemma starfun_exp_add_HFinite_Infinitesimal_approx: |