src/HOLCF/Ssum.thy
changeset 17817 405fb812e738
parent 16921 16094ed8ac6b
child 17837 2922be3544f8
equal deleted inserted replaced
17816:9942c5ed866a 17817:405fb812e738
    13 
    13 
    14 defaultsort pcpo
    14 defaultsort pcpo
    15 
    15 
    16 subsection {* Definition of strict sum type *}
    16 subsection {* Definition of strict sum type *}
    17 
    17 
    18 pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
    18 pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
    19         "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
    19         "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
    20 by simp
    20 by simp
    21 
    21 
    22 syntax (xsymbols)
    22 syntax (xsymbols)
    23   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
    23   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)