added append (curried);
authorwenzelm
Fri Feb 13 20:16:02 1998 +0100 (1998-02-13)
changeset 4629401dd9b1b548
parent 4628 0c7e97836e3c
child 4630 437ddddbfef5
added append (curried);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Feb 12 17:53:05 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Feb 13 20:16:02 1998 +0100
     1.3 @@ -69,6 +69,7 @@
     1.4    val hd: 'a list -> 'a
     1.5    val tl: 'a list -> 'a list
     1.6    val cons: 'a -> 'a list -> 'a list
     1.7 +  val append: 'a list -> 'a list -> 'a list
     1.8    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
     1.9    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.10    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.11 @@ -382,6 +383,8 @@
    1.12  
    1.13  fun cons x xs = x :: xs;
    1.14  
    1.15 +fun append xs ys = xs @ ys;
    1.16 +
    1.17  
    1.18  (* fold *)
    1.19