diff -r 000000000000 -r a5a9c433f639 src/CCL/ex/List.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/ex/List.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,44 @@
+(*  Title: 	CCL/ex/list.thy
+    ID:         $Id$
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Programs defined over lists.
+*)
+
+List = Nat + 
+
+consts
+  map       :: "[i=>i,i]=>i"
+  "o"       :: "[i=>i,i=>i]=>i=>i"             (infixr 55)
+  "@"       :: "[i,i]=>i"             (infixr 55)
+  mem       :: "[i,i]=>i"             (infixr 55)
+  filter    :: "[i,i]=>i"
+  flat      :: "i=>i"
+  partition :: "[i,i]=>i"
+  insert    :: "[i,i,i]=>i"
+  isort     :: "i=>i"
+  qsort     :: "i=>i"
+
+rules 
+
+  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x).g)"
+  comp_def    "f o g == (%x.f(g(x)))"
+  append_def  "l @ m == lrec(l,m,%x xs g.x.g)"
+  mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
+  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
+  flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
+
+  insert_def  "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
+  isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
+
+  partition_def 
+  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
+\                            if f`x then part(xs,x.a,b) else part(xs,a,x.b)) \
+\                    in part(l,[],[])"
+  qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
+\                                   let p be partition(f`h,t) \
+\                                   in split(p,%x y.qsortx(x) @ h.qsortx(y))) \
+\                          in qsortx(l)"
+
+end