# HG changeset patch # User wenzelm # Date 887397362 -3600 # Node ID 401dd9b1b5484feff7ca8d40c1d005892a7cb6ed # Parent 0c7e97836e3c1059e7851dcf49d4e04f8bb4c1c2 added append (curried); diff -r 0c7e97836e3c -r 401dd9b1b548 src/Pure/library.ML --- a/src/Pure/library.ML Thu Feb 12 17:53:05 1998 +0100 +++ b/src/Pure/library.ML Fri Feb 13 20:16:02 1998 +0100 @@ -69,6 +69,7 @@ val hd: 'a list -> 'a val tl: 'a list -> 'a list val cons: 'a -> 'a list -> 'a list + val append: 'a list -> 'a list -> 'a list val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a @@ -382,6 +383,8 @@ fun cons x xs = x :: xs; +fun append xs ys = xs @ ys; + (* fold *)