--- a/src/HOL/Orderings.thy Wed Jan 10 15:57:55 2018 +0100
+++ b/src/HOL/Orderings.thy Wed Jan 10 18:18:34 2018 +0100
@@ -132,10 +132,8 @@
begin
notation
- less_eq ("'(\<le>')") and
- less_eq ("(_/ \<le> _)" [51, 51] 50) and
- less ("'(<')") and
- less ("(_/ < _)" [51, 51] 50)
+ less_eq (infix "\<le>" 50) and
+ less (infix "<" 50)
abbreviation (input)
greater_eq (infix "\<ge>" 50)
@@ -146,8 +144,7 @@
where "x > y \<equiv> y < x"
notation (ASCII)
- less_eq ("'(<=')") and
- less_eq ("(_/ <= _)" [51, 51] 50)
+ less_eq (infix "<=" 50)
notation (input)
greater_eq (infix ">=" 50)
--- a/src/HOL/Set.thy Wed Jan 10 15:57:55 2018 +0100
+++ b/src/HOL/Set.thy Wed Jan 10 18:18:34 2018 +0100
@@ -20,20 +20,16 @@
and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
notation
- member ("'(\<in>')") and
- member ("(_/ \<in> _)" [51, 51] 50)
+ member (infix "\<in>" 50)
abbreviation not_member
where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
notation
- not_member ("'(\<notin>')") and
- not_member ("(_/ \<notin> _)" [51, 51] 50)
+ not_member (infix "\<notin>" 50)
notation (ASCII)
- member ("'(:')") and
- member ("(_/ : _)" [51, 51] 50) and
- not_member ("'(~:')") and
- not_member ("(_/ ~: _)" [51, 51] 50)
+ member (infix ":" 50) and
+ not_member (infix "~:" 50)
text \<open>Set comprehensions\<close>