# HG changeset patch
# User nipkow
# Date 1515662022 -3600
# Node ID 90fe8c635ba02f56865e69a9b4d1646f59714ee5
# Parent  b71431a2051ee7709ccd1c2e6b6a3ce87a87ad91
line break before op was intentional

diff -r b71431a2051e -r 90fe8c635ba0 src/HOL/Orderings.thy
--- 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)
diff -r b71431a2051e -r 90fe8c635ba0 src/HOL/Set.thy
--- 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>