# HG changeset patch
# User nipkow
# Date 1515604714 -3600
# Node ID a82df75b7f85f6c9062856028d6fa07f3e42bf76
# Parent  bbed46f40cf56354cea7882af005a37993b4eed5
tuned notation

diff -r bbed46f40cf5 -r a82df75b7f85 src/HOL/Orderings.thy
--- 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)
diff -r bbed46f40cf5 -r a82df75b7f85 src/HOL/Set.thy
--- 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>