added oooo;
authorwenzelm
Tue Apr 27 10:42:08 1999 +0200 (1999-04-27)
changeset 6510b5ef6d115b45
parent 6509 9f7f4fd05b1f
child 6511 11b07125422e
added oooo;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Apr 26 13:25:49 1999 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Apr 27 10:42:08 1999 +0200
     1.3 @@ -12,7 +12,7 @@
     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 +infix 3 oo ooo oooo;
     1.9  
    1.10  signature LIBRARY =
    1.11  sig
    1.12 @@ -27,6 +27,7 @@
    1.13    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.14    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.15    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.16 +  val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.17  
    1.18    (*stamps*)
    1.19    type stamp
    1.20 @@ -281,6 +282,8 @@
    1.21  (*concatenation: 2 and 3 args*)
    1.22  fun (f oo g) x y = f (g x y);
    1.23  fun (f ooo g) x y z = f (g x y z);
    1.24 +fun (f oooo g) x y z w = f (g x y z w);
    1.25 +
    1.26  
    1.27  
    1.28  (** stamps **)