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