--- a/src/HOL/Orderings.thy Wed Jan 10 20:17:36 2018 +0100
+++ b/src/HOL/Orderings.thy Thu Jan 11 10:13:42 2018 +0100
@@ -132,8 +132,10 @@
begin
notation
- less_eq (infix "\<le>" 50) and
- less (infix "<" 50)
+ less_eq ("'(\<le>')") and
+ less_eq ("(_/ \<le> _)" [51, 51] 50) and
+ less ("'(<')") and
+ less ("(_/ < _)" [51, 51] 50)
abbreviation (input)
greater_eq (infix "\<ge>" 50)
@@ -144,7 +146,8 @@
where "x > y \<equiv> y < x"
notation (ASCII)
- less_eq (infix "<=" 50)
+ less_eq ("'(<=')") and
+ less_eq ("(_/ <= _)" [51, 51] 50)
notation (input)
greater_eq (infix ">=" 50)
--- 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>