added append (curried);
authorwenzelm
Fri, 13 Feb 1998 20:16:02 +0100
changeset 4629 401dd9b1b548
parent 4628 0c7e97836e3c
child 4630 437ddddbfef5
added append (curried);
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 *)