--- a/src/HOL/Set.thy Wed Jan 10 20:17:36 2018 +0100
+++ b/src/HOL/Set.thy Thu Jan 11 10:13:42 2018 +0100
@@ -20,16 +20,20 @@
and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
notation
- member (infix "\<in>" 50)
+ member ("'(\<in>')") and
+ member ("(_/ \<in> _)" [51, 51] 50)
abbreviation not_member
where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
notation
- not_member (infix "\<notin>" 50)
+ not_member ("'(\<notin>')") and
+ not_member ("(_/ \<notin> _)" [51, 51] 50)
notation (ASCII)
- member (infix ":" 50) and
- not_member (infix "~:" 50)
+ member ("'(:')") and
+ member ("(_/ : _)" [51, 51] 50) and
+ not_member ("'(~:')") and
+ not_member ("(_/ ~: _)" [51, 51] 50)
text \<open>Set comprehensions\<close>