diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -1944,7 +1944,7 @@
       using \<open>u + v = 1\<close> by auto
     ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
       using h1 by auto
-    then have "u *\<^sub>R x + v *\<^sub>R y : S" by auto
+    then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto
   }
   then show ?thesis unfolding affine_def by auto
 qed
@@ -2031,7 +2031,7 @@
   have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
   have "affine ((\<lambda>x. (-a)+x) ` S)"
     using  affine_translation assms by auto
-  moreover have "0 : ((\<lambda>x. (-a)+x) ` S)"
+  moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
     using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
   ultimately show ?thesis using subspace_affine by auto
 qed
@@ -2130,7 +2130,7 @@
 
 lemma mem_cone:
   assumes "cone S" "x \<in> S" "c \<ge> 0"
-  shows "c *\<^sub>R x : S"
+  shows "c *\<^sub>R x \<in> S"
   using assms cone_def[of S] by auto
 
 lemma cone_contains_0:
@@ -3409,7 +3409,7 @@
   assumes "a \<notin> S"
   shows "affine_dependent (insert a S) \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` S)"
 proof -
-  have "((+) (- a) ` S) = {x - a| x . x : S}" by auto
+  have "((+) (- a) ` S) = {x - a| x . x \<in> S}" by auto
   then show ?thesis
     using affine_dependent_translation_eq[of "(insert a S)" "-a"]
       affine_dependent_imp_dependent2 assms