src/HOL/IMP/Abs_State.thy

--- a/src/HOL/IMP/Abs_State.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -157,7 +157,7 @@
 by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
 
 lemma in_gamma_option_iff:
-  "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
+  "x \<in> \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x \<in> r u')"
 by (cases u) auto
 
 end