src/HOL/Nonstandard_Analysis/HyperNat.thy
changeset 64438 f91cae6c1d74
parent 64435 c93b0e6131c3
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Nov 01 00:55:52 2016 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Nov 01 01:04:53 2016 +0100
     1.3 @@ -329,18 +329,18 @@
     1.4  subsubsection \<open>Alternative Characterization of @{term HNatInfinite} using Free Ultrafilter\<close>
     1.5  
     1.6  lemma HNatInfinite_FreeUltrafilterNat:
     1.7 -  "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
     1.8 +  "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
     1.9    apply (auto simp add: HNatInfinite_iff SHNat_eq)
    1.10    apply (drule_tac x="star_of u" in spec, simp)
    1.11    apply (simp add: star_of_def star_less_def starP2_star_n)
    1.12    done
    1.13  
    1.14  lemma FreeUltrafilterNat_HNatInfinite:
    1.15 -  "\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat \<Longrightarrow> star_n X \<in> HNatInfinite"
    1.16 +  "\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
    1.17    by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    1.18  
    1.19  lemma HNatInfinite_FreeUltrafilterNat_iff:
    1.20 -  "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
    1.21 +  "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) \<U>)"
    1.22    by (rule iffI [OF HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite])
    1.23  
    1.24