src/HOL/Analysis/Sparse_In.thy

 definition cosparse :: "'a set \<Rightarrow> 'a :: topological_space filter" where
  "cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
 
 syntax
   "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  ("(3\<forall>\<^sub>\<approx>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_eventually_cosparse" == eventually
 translations
   "\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
 
 syntax
   "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3\<forall>\<^sub>\<approx>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_qeventually_cosparse" == eventually
 translations
   "\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"
 
 print_translation \<open>
 let