src/HOLCF/Ssum0.thy
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)"