| author | wenzelm | 
| Tue, 05 Oct 1999 15:30:14 +0200 | |
| changeset 7718 | 86755cc5b83c | 
| parent 6810 | 731c848f6f0c | 
| child 12338 | de0f4a63baa5 | 
| 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  | 
|
11  | 
instance list :: (term) order  | 
|
12  | 
(prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)  | 
|
13  | 
||
14  | 
end  |