equal
deleted
inserted
replaced
240 |
240 |
241 instance udom :: pcpo |
241 instance udom :: pcpo |
242 by intro_classes (fast intro: udom_minimal) |
242 by intro_classes (fast intro: udom_minimal) |
243 |
243 |
244 lemma inst_udom_pcpo: "\<bottom> = udom_principal 0" |
244 lemma inst_udom_pcpo: "\<bottom> = udom_principal 0" |
245 by (rule udom_minimal [THEN UU_I, symmetric]) |
245 by (rule udom_minimal [THEN bottomI, symmetric]) |
246 |
246 |
247 |
247 |
248 subsection {* Compact bases of domains *} |
248 subsection {* Compact bases of domains *} |
249 |
249 |
250 typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" |
250 typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" |