author | nipkow |
Wed, 02 Sep 1998 16:52:06 +0200 | |
changeset 5425 | 157c6663dedd |
parent 5261 | ce3c25c8a694 |
child 9102 | c7ba07e3bbe8 |
permissions | -rw-r--r-- |
5261 | 1 |
(* Title: HOL/Lambda/ListOrder.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TU Muenchen |
|
5 |
||
6 |
Lifting an order to lists of elements, relating exactly one element |
|
7 |
*) |
|
8 |
||
9 |
ListOrder = List + Acc + |
|
10 |
||
11 |
constdefs |
|
12 |
step1 :: "('a * 'a)set => ('a list * 'a list)set" |
|
13 |
"step1 r == |
|
14 |
{(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}" |
|
15 |
||
16 |
end |