author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 6810 | 731c848f6f0c |
child 13798 | 4c1a53627500 |
permissions | -rw-r--r-- |
6708 | 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 |
||
6810 | 9 |
ListOrder = GenPrefix + |
6708 | 10 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
6810
diff
changeset
|
11 |
instance list :: (type) order |
6708 | 12 |
(prefix_refl,prefix_trans,prefix_antisym,prefix_less_le) |
13 |
||
14 |
end |