--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListOrder.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Lambda/ListOrder.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Lifting an order to lists of elements, relating exactly one element
+*)
+
+ListOrder = List + Acc +
+
+constdefs
+ step1 :: "('a * 'a)set => ('a list * 'a list)set"
+"step1 r ==
+   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"
+
+end