| changeset 9102 | c7ba07e3bbe8 |
| parent 5261 | ce3c25c8a694 |
| child 9771 | 54c6a2c6e569 |
--- a/src/HOL/Lambda/ListOrder.thy Wed Jun 21 18:09:09 2000 +0200 +++ b/src/HOL/Lambda/ListOrder.thy Wed Jun 21 18:14:28 2000 +0200 @@ -6,7 +6,7 @@ Lifting an order to lists of elements, relating exactly one element *) -ListOrder = List + Acc + +ListOrder = Acc + constdefs step1 :: "('a * 'a)set => ('a list * 'a list)set"