changeset 6708 | 62beb3336b02 |
child 6810 | 731c848f6f0c |
6707:3b07e62a718c | 6708:62beb3336b02 |
---|---|
1 (* Title: HOL/UNITY/ListOrder |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Lists are partially ordered by the prefix relation |
|
7 *) |
|
8 |
|
9 ListOrder = Prefix + |
|
10 |
|
11 instance list :: (term) order |
|
12 (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le) |
|
13 |
|
14 end |