src/HOL/Filter.thy
changeset 61378 3e04c9ca001a
parent 61245 b77bf45efe21
child 61531 ab2e862263e7
     1.1 --- a/src/HOL/Filter.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -698,10 +698,6 @@
     1.4    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
     1.5    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
     1.6  
     1.7 -notation (HTML output)
     1.8 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
     1.9 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    1.10 -
    1.11  lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
    1.12    unfolding cofinite_def
    1.13  proof (rule eventually_Abs_filter, rule is_filter.intro)