equal
deleted
inserted
replaced
211 apply intro_classes |
211 apply intro_classes |
212 apply (erule compact_imp_max_in_chain) |
212 apply (erule compact_imp_max_in_chain) |
213 apply (case_tac "\<Squnion>i. Y i", simp_all) |
213 apply (case_tac "\<Squnion>i. Y i", simp_all) |
214 done |
214 done |
215 |
215 |
216 instance sum :: (finite_po, finite_po) finite_po .. |
|
217 |
|
218 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo |
216 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo |
219 by intro_classes (simp add: below_sum_def split: sum.split) |
217 by intro_classes (simp add: below_sum_def split: sum.split) |
220 |
218 |
221 end |
219 end |