src/HOL/UNITY/ListOrder.thy
changeset 6708 62beb3336b02
child 6810 731c848f6f0c
equal deleted inserted replaced
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