# HG changeset patch
# User paulson
# Date 927553677 -7200
# Node ID 62beb3336b02fdf46ebe37e8f24f9a69f2325fa3
# Parent  3b07e62a718c007eaf7193846e4aadc658fcae98
lists are partially ordered by the prefix relation

diff -r 3b07e62a718c -r 62beb3336b02 src/HOL/UNITY/ListOrder.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ListOrder.thy	Mon May 24 15:47:57 1999 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/UNITY/ListOrder
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Lists are partially ordered by the prefix relation
+*)
+
+ListOrder = Prefix +
+
+instance list :: (term) order
+    (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
+
+end