--- a/src/HOL/Complex.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Complex.thy Thu Nov 08 09:11:52 2018 +0100
@@ -308,7 +308,7 @@
definition dist_complex_def: "dist x y = cmod (x - y)"
definition uniformity_complex_def [code del]:
- "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity :: (complex \<times> complex) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_complex_def [code del]:
"open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"