added oooo;
authorwenzelm
Tue, 27 Apr 1999 10:42:08 +0200
changeset 6510 b5ef6d115b45
parent 6509 9f7f4fd05b1f
child 6511 11b07125422e
added oooo;
src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Apr 26 13:25:49 1999 +0200
+++ b/src/Pure/library.ML	Tue Apr 27 10:42:08 1999 +0200
@@ -12,7 +12,7 @@
   mem mem_int mem_string union union_int union_string inter inter_int
   inter_string subset subset_int subset_string;
 
-infix 3 oo ooo;
+infix 3 oo ooo oooo;
 
 signature LIBRARY =
 sig
@@ -27,6 +27,7 @@
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
+  val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
 
   (*stamps*)
   type stamp
@@ -281,6 +282,8 @@
 (*concatenation: 2 and 3 args*)
 fun (f oo g) x y = f (g x y);
 fun (f ooo g) x y z = f (g x y z);
+fun (f oooo g) x y z w = f (g x y z w);
+
 
 
 (** stamps **)