# HG changeset patch
# User wenzelm
# Date 1435309624 -7200
# Node ID 1d31e3a503739e051005632562f7b96a08c0ad50
# Parent  48fdff264eb2be9c29d8914e2f34cb5a456340e4
proper spacing, as for other syntax for these symbols;

diff -r 48fdff264eb2 -r 1d31e3a50373 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Fri Jun 26 11:07:04 2015 +0200
@@ -126,7 +126,7 @@
   "LUB n. t n == lub (range t)"
 
 notation (xsymbols)
-  Lub  (binder "\<Squnion> " 10)
+  Lub  (binder "\<Squnion>" 10)
 
 text {* access to some definition as inference rule *}
 
diff -r 48fdff264eb2 -r 1d31e3a50373 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/Set_Interval.thy	Fri Jun 26 11:07:04 2015 +0200
@@ -66,10 +66,10 @@
   "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
 
 syntax (xsymbols)
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
 
 syntax (latex output)
   "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
diff -r 48fdff264eb2 -r 1d31e3a50373 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Fri Jun 26 10:20:33 2015 +0200
+++ b/src/HOL/UNITY/Union.thy	Fri Jun 26 11:07:04 2015 +0200
@@ -47,8 +47,8 @@
   "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
 syntax (xsymbols)
-  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
-  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
+  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
+  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion>_\<in>_./ _)" 10)
 
 translations
   "JN x: A. B" == "CONST JOIN A (%x. B)"