author | wenzelm |
Tue, 24 Nov 1998 12:03:09 +0100 | |
changeset 5953 | d6017ce6b93e |
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