added oo, ooo (*concatenation: 2 and 3 args*);
authorwenzelm
Mon Nov 16 11:32:28 1998 +0100 (1998-11-16)
changeset 5893c755dfd02509
parent 5892 e5e44cc54eb2
child 5894 71667e5c2ff8
added oo, ooo (*concatenation: 2 and 3 args*);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Nov 16 11:14:44 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 16 11:32:28 1998 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4    mem mem_int mem_string union union_int union_string inter inter_int
     1.5    inter_string subset subset_int subset_string;
     1.6  
     1.7 +infix 3 oo ooo;
     1.8 +
     1.9  signature LIBRARY =
    1.10  sig
    1.11    (*functions*)
    1.12 @@ -23,6 +25,8 @@
    1.13    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.14    val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    1.15    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.16 +  val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.17 +  val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.18  
    1.19    (*stamps*)
    1.20    type stamp
    1.21 @@ -268,6 +272,9 @@
    1.22          | rep (n, x) = rep (n - 1, f x)
    1.23    in rep (n, x) end;
    1.24  
    1.25 +(*concatenation: 2 and 3 args*)
    1.26 +fun (f oo g) x y = f (g x y);
    1.27 +fun (f ooo g) x y z = f (g x y z);
    1.28  
    1.29  
    1.30  (** stamps **)