--- 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)"