src/HOL/NSA/HyperNat.thy

 
 
 subsection\<open>Existence of an infinite hypernatural number\<close>
 
 definition
-  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+  (* \<omega> is in fact an infinite hypernatural number = [<1,2,3,...>] *)
   whn :: hypnat where
   hypnat_omega_def: "whn = star_n (%n::nat. n)"
 
 lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
 by (simp add: FreeUltrafilterNat.singleton' hypnat_omega_def star_of_def star_n_eq_iff)