# HG changeset patch
# User huffman
# Date 1159075096 -7200
# Node ID 1cc6fefbff1a8c28cd22c7ef7a49b23bf96bf215
# Parent  76c49548d14c0ed1030854bab31f767e3c046760
moved SEQ_Infinitesimal from SEQ to HyperNat

diff -r 76c49548d14c -r 1cc6fefbff1a src/HOL/Hyperreal/HyperNat.thy
--- 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]) 
diff -r 76c49548d14c -r 1cc6fefbff1a src/HOL/Hyperreal/SEQ.thy
--- 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: