--- a/src/HOLCF/Sprod.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Sprod.thy Wed Mar 03 16:43:55 2010 +0100
@@ -22,10 +22,10 @@
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
-syntax (xsymbols)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
-syntax (HTML output)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (xsymbols)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (HTML output)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
"(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"