src/HOL/Hyperreal/SEQ.thy
changeset 17429 e8d6ed3aacfe
parent 17318 bc1c75855f3d
child 17439 a358da1a0218
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:16:04 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:46:22 2005 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  lemma SEQ_Infinitesimal:
     1.5        "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
     1.6  apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
     1.7 -apply (simp add: star_n_inverse2)
     1.8 +apply (simp add: star_n_inverse)
     1.9  apply (rule bexI [OF _ Rep_star_star_n])
    1.10  apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
    1.11  done