--- a/src/HOL/Hyperreal/HyperNat.thy Sun Sep 24 07:14:02 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Sun Sep 24 07:18:16 2006 +0200
@@ -157,6 +157,16 @@
follows because member @{term FreeUltrafilterNat} is not finite.
See @{text HyperDef.thy} for similar argument.*}
+text{* Example of an hypersequence (i.e. an extended standard sequence)
+ whose term with an hypernatural suffix is an infinitesimal i.e.
+ the whn'nth term of the hypersequence is a member of Infinitesimal*}
+
+lemma SEQ_Infinitesimal:
+ "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
+apply (simp add: hypnat_omega_def starfun star_n_inverse)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
+done
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
apply (insert finite_atMost [of m])
--- a/src/HOL/Hyperreal/SEQ.thy Sun Sep 24 07:14:02 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Sun Sep 24 07:18:16 2006 +0200
@@ -65,20 +65,6 @@
"NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
-declare real_norm_def [simp]
-
-text{* Example of an hypersequence (i.e. an extended standard sequence)
- whose term with an hypernatural suffix is an infinitesimal i.e.
- the whn'nth term of the hypersequence is a member of Infinitesimal*}
-
-lemma SEQ_Infinitesimal:
- "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def starfun star_n_inverse)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
-done
-
-
subsection{*LIMSEQ and NSLIMSEQ*}
lemma LIMSEQ_iff: