author | wenzelm |
Tue, 27 Apr 1999 10:45:20 +0200 | |
changeset 6516 | 09207771cc7c |
parent 5261 | ce3c25c8a694 |
child 9102 | c7ba07e3bbe8 |
permissions | -rw-r--r-- |
(* 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