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