| changeset 19564 | d3e2f532459a |
| parent 19086 | 1b3780be6cc2 |
| child 20503 | 503ac4c5ef91 |
| 19563:ddd36d9e6943 | 19564:d3e2f532459a |
|---|---|
4 Copyright 1998 TU Muenchen |
4 Copyright 1998 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* Lifting an order to lists of elements *} |
7 header {* Lifting an order to lists of elements *} |
8 |
8 |
9 theory ListOrder imports Accessible_Part begin |
9 theory ListOrder imports Main begin |
10 |
10 |
11 text {* |
11 text {* |
12 Lifting an order to lists of elements, relating exactly one |
12 Lifting an order to lists of elements, relating exactly one |
13 element. |
13 element. |
14 *} |
14 *} |