src/HOLCF/Sprod.thy
changeset 17817 405fb812e738
parent 16920 ded12c9e88c2
child 17837 2922be3544f8
     1.1 --- a/src/HOLCF/Sprod.thy	Mon Oct 10 05:30:02 2005 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Mon Oct 10 05:46:17 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  subsection {* Definition of strict product type *}
     1.6  
     1.7 -pcpodef (Sprod)  ('a, 'b) "**" (infixr 20) =
     1.8 +pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
     1.9          "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
    1.10  by simp
    1.11