src/HOLCF/Ssum0.thy
changeset 12114 a8e860c86252
parent 12030 46d57d0290a2
child 14565 c6dc17aab88a
     1.1 --- a/src/HOLCF/Ssum0.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOLCF/Ssum0.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
     1.5  	"{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    1.10  
    1.11  consts