
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -45,7 +45,7 @@
   is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
 
 definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
-  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
   where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"




