equal
deleted
inserted
replaced
20 by (rule typedef_finite_po [OF type_definition_Sprod]) |
20 by (rule typedef_finite_po [OF type_definition_Sprod]) |
21 |
21 |
22 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
22 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
23 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def]) |
23 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def]) |
24 |
24 |
25 syntax (xsymbols) |
25 type_notation (xsymbols) |
26 "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
26 "**" ("(_ \<otimes>/ _)" [21,20] 20) |
27 syntax (HTML output) |
27 type_notation (HTML output) |
28 "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
28 "**" ("(_ \<otimes>/ _)" [21,20] 20) |
29 |
29 |
30 lemma spair_lemma: |
30 lemma spair_lemma: |
31 "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod" |
31 "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod" |
32 by (simp add: Sprod_def strictify_conv_if) |
32 by (simp add: Sprod_def strictify_conv_if) |
33 |
33 |