src/HOLCF/Sprod.thy
changeset 35547 991a6af75978
parent 35525 fa231b86cb1e
parent 35427 ad039d29e01c
child 35783 38538bfe9ca6
     1.1 --- a/src/HOLCF/Sprod.thy	Wed Mar 03 15:19:34 2010 +0100
     1.2 +++ b/src/HOLCF/Sprod.thy	Wed Mar 03 16:43:55 2010 +0100
     1.3 @@ -22,10 +22,10 @@
     1.4  instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
     1.5  by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
     1.9 -syntax (HTML output)
    1.10 -  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    1.11 +type_notation (xsymbols)
    1.12 +  sprod  ("(_ \<otimes>/ _)" [21,20] 20)
    1.13 +type_notation (HTML output)
    1.14 +  sprod  ("(_ \<otimes>/ _)" [21,20] 20)
    1.15  
    1.16  lemma spair_lemma:
    1.17    "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"