src/HOL/Library/Going_To_Filter.thy
changeset 69597 ff784d5a5bfb
parent 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Going_To_Filter.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Library/Going_To_Filter.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4  begin
     1.5  
     1.6  definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter"
     1.7 -  ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where
     1.8 +  (\<open>(_)/ going'_to (_)/ within (_)\<close> [1000,60,60] 60) where
     1.9    "f going_to F within A = inf (filtercomap f F) (principal A)"
    1.10  
    1.11  abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter"
    1.12 -    (infix "going'_to" 60)
    1.13 +    (infix \<open>going'_to\<close> 60)
    1.14      where "f going_to F \<equiv> f going_to F within UNIV"
    1.15  
    1.16  text \<open>