--- a/src/HOLCF/Ssum.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Ssum.thy Wed Mar 03 16:43:55 2010 +0100
@@ -24,10 +24,11 @@
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
-syntax (xsymbols)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
-syntax (HTML output)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (HTML output)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+
subsection {* Definitions of constructors *}