src/HOL/Library/Infinite_Set.thy
changeset 21210 c17fd2df4e9e
parent 20809 6c4fd0b4b63a
child 21256 47195501ecf7
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -354,11 +354,11 @@
     1.4    Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
     1.5    "Alm_all P = (\<not> (INF x. \<not> P x))"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
    1.10    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    1.11  
    1.12 -const_syntax (HTML output)
    1.13 +notation (HTML output)
    1.14    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
    1.15    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    1.16