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