changeset 14565 | c6dc17aab88a |
parent 12114 | a8e860c86252 |
child 14981 | e73f8140af78 |
1.1 --- a/src/HOLCF/Ssum0.thy Wed Apr 14 13:28:46 2004 +0200 1.2 +++ b/src/HOLCF/Ssum0.thy Wed Apr 14 14:13:05 2004 +0200 1.3 @@ -19,6 +19,8 @@ 1.4 1.5 syntax (xsymbols) 1.6 "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20) 1.7 +syntax (HTML output) 1.8 + "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20) 1.9 1.10 consts 1.11 Isinl :: "'a => ('a ++ 'b)"