src/HOLCF/Ssum.thy
changeset 35427 ad039d29e01c
parent 33808 31169fdc5ae7
child 35547 991a6af75978
--- a/src/HOLCF/Ssum.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/Ssum.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -24,10 +24,10 @@
 instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
 
-syntax (xsymbols)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
-syntax (HTML output)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (HTML output)
+  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
 
 subsection {* Definitions of constructors *}