| changeset 62858 | d72a6f9ee690 |
| parent 62837 | 237ef2bab6c7 |
| child 63040 | eb4ddd18d635 |
| 62857:a8758f47f9e8 | 62858:d72a6f9ee690 |
|---|---|
1 (* Title: src/HOL/Library/Complete_Partial_Order2 |
1 (* Title: HOL/Library/Complete_Partial_Order2.thy |
2 Author: Andreas Lochbihler, ETH Zurich |
2 Author: Andreas Lochbihler, ETH Zurich |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close> |
5 section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close> |
6 |
6 |