changeset 55579 | 207538943038 |
parent 54538 | ba7392b52a7c |
child 58881 | b9556a055632 |
55578:32774e40afb0 | 55579:207538943038 |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Prefix order on lists as order class instance *} |
5 header {* Prefix order on lists as order class instance *} |
6 |
6 |
7 theory Prefix_Order |
7 theory Prefix_Order |
8 imports List_Prefix |
8 imports Sublist |
9 begin |
9 begin |
10 |
10 |
11 instantiation list :: (type) order |
11 instantiation list :: (type) order |
12 begin |
12 begin |
13 |
13 |