# HG changeset patch
# User huffman
# Date 1166042794 -3600
# Node ID e3a7205fcb011201afd316d5b1b5307b10eaa10a
# Parent  54018ed3b99d857b88f878784a8002838bbf7d00
remove use of FreeUltrafilterNat

diff -r 54018ed3b99d -r e3a7205fcb01 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 21:25:56 2006 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 21:46:34 2006 +0100
@@ -361,11 +361,18 @@
 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
 by (transfer, rule ln_inverse)
 
+lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) x\<bar> = ( *f* exp) x"
+by transfer (rule abs_exp_cancel)
+
+lemma starfun_exp_less_mono: "\<And>x y. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
+by transfer (rule exp_less_mono)
+
 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
-apply (cases x)
-apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule_tac x = "exp u" in exI)
-apply ultra
+apply (auto simp add: HFinite_def, rename_tac u)
+apply (rule_tac x="( *f* exp) u" in rev_bexI)
+apply (simp add: Reals_eq_Standard)
+apply (simp add: starfun_abs_exp_cancel)
+apply (simp add: starfun_exp_less_mono)
 done
 
 lemma starfun_exp_add_HFinite_Infinitesimal_approx: