changeset 10264 | ef384b242d09 |
parent 9941 | fe05af7ec816 |
child 11639 | 4213422388c4 |
10263:9cc180732945 | 10264:ef384b242d09 |
---|---|
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 = Acc: |
9 theory ListOrder = Accessible_Part: |
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 *} |