use symbols by default;
authorwenzelm
Mon Dec 28 18:03:26 2015 +0100 (2015-12-28)
changeset 619537247cb62406c
parent 61952 546958347e05
child 61954 1d43f86f48be
use symbols by default;
src/HOL/Filter.thy
     1.1 --- a/src/HOL/Filter.thy	Mon Dec 28 17:43:30 2015 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Dec 28 18:03:26 2015 +0100
     1.3 @@ -39,9 +39,8 @@
     1.4  definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
     1.5    where "eventually P F \<longleftrightarrow> Rep_filter F P"
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
     1.9 -
    1.10 +syntax
    1.11 +  "_eventually" :: "pttrn => 'a filter => bool => bool"  ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.12  translations
    1.13    "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
    1.14  
    1.15 @@ -150,9 +149,8 @@
    1.16  definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.17    where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
    1.18  
    1.19 -syntax (xsymbols)
    1.20 -  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.21 -
    1.22 +syntax
    1.23 +  "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.24  translations
    1.25    "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
    1.26