proper spacing, as for other syntax for these symbols;
authorwenzelm
Fri Jun 26 11:07:04 2015 +0200 (2015-06-26)
changeset 605861d31e3a50373
parent 60585 48fdff264eb2
child 60587 0318b43ee95c
proper spacing, as for other syntax for these symbols;
src/HOL/HOLCF/Porder.thy
src/HOL/Set_Interval.thy
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/HOLCF/Porder.thy	Fri Jun 26 10:20:33 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Porder.thy	Fri Jun 26 11:07:04 2015 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    "LUB n. t n == lub (range t)"
     1.5  
     1.6  notation (xsymbols)
     1.7 -  Lub  (binder "\<Squnion> " 10)
     1.8 +  Lub  (binder "\<Squnion>" 10)
     1.9  
    1.10  text {* access to some definition as inference rule *}
    1.11  
     2.1 --- a/src/HOL/Set_Interval.thy	Fri Jun 26 10:20:33 2015 +0200
     2.2 +++ b/src/HOL/Set_Interval.thy	Fri Jun 26 11:07:04 2015 +0200
     2.3 @@ -66,10 +66,10 @@
     2.4    "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
     2.5  
     2.6  syntax (xsymbols)
     2.7 -  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
     2.8 -  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
     2.9 -  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
    2.10 -  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
    2.11 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
    2.12 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
    2.13 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
    2.14 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
    2.15  
    2.16  syntax (latex output)
    2.17    "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
     3.1 --- a/src/HOL/UNITY/Union.thy	Fri Jun 26 10:20:33 2015 +0200
     3.2 +++ b/src/HOL/UNITY/Union.thy	Fri Jun 26 11:07:04 2015 +0200
     3.3 @@ -47,8 +47,8 @@
     3.4    "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
     3.5    "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
     3.6  syntax (xsymbols)
     3.7 -  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
     3.8 -  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
     3.9 +  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
    3.10 +  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion>_\<in>_./ _)" 10)
    3.11  
    3.12  translations
    3.13    "JN x: A. B" == "CONST JOIN A (%x. B)"