equal
deleted
inserted
replaced
22 by (rule typedef_finite_po [OF type_definition_Ssum]) |
22 by (rule typedef_finite_po [OF type_definition_Ssum]) |
23 |
23 |
24 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
24 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
25 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def]) |
25 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def]) |
26 |
26 |
27 syntax (xsymbols) |
27 type_notation (xsymbols) |
28 ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
28 ssum ("(_ \<oplus>/ _)" [21, 20] 20) |
29 syntax (HTML output) |
29 type_notation (HTML output) |
30 ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
30 ssum ("(_ \<oplus>/ _)" [21, 20] 20) |
|
31 |
31 |
32 |
32 subsection {* Definitions of constructors *} |
33 subsection {* Definitions of constructors *} |
33 |
34 |
34 definition |
35 definition |
35 sinl :: "'a \<rightarrow> ('a ++ 'b)" where |
36 sinl :: "'a \<rightarrow> ('a ++ 'b)" where |