equal
deleted
inserted
replaced
159 |
159 |
160 instance convex_pd :: (bifinite) pcpo |
160 instance convex_pd :: (bifinite) pcpo |
161 by intro_classes (fast intro: convex_pd_minimal) |
161 by intro_classes (fast intro: convex_pd_minimal) |
162 |
162 |
163 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)" |
163 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)" |
164 by (rule convex_pd_minimal [THEN UU_I, symmetric]) |
164 by (rule convex_pd_minimal [THEN bottomI, symmetric]) |
165 |
165 |
166 |
166 |
167 subsection {* Monadic unit and plus *} |
167 subsection {* Monadic unit and plus *} |
168 |
168 |
169 definition |
169 definition |