src/Pure/library.ML
changeset 5893 c755dfd02509
parent 5285 2d1425492fb3
child 5904 e077a0e66563
equal deleted inserted replaced
5892:e5e44cc54eb2 5893:c755dfd02509
     9 *)
     9 *)
    10 
    10 
    11 infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    11 infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    12   mem mem_int mem_string union union_int union_string inter inter_int
    12   mem mem_int mem_string union union_int union_string inter inter_int
    13   inter_string subset subset_int subset_string;
    13   inter_string subset subset_int subset_string;
       
    14 
       
    15 infix 3 oo ooo;
    14 
    16 
    15 signature LIBRARY =
    17 signature LIBRARY =
    16 sig
    18 sig
    17   (*functions*)
    19   (*functions*)
    18   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    20   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    21   val K: 'a -> 'b -> 'a
    23   val K: 'a -> 'b -> 'a
    22   val |> : 'a * ('a -> 'b) -> 'b
    24   val |> : 'a * ('a -> 'b) -> 'b
    23   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    25   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    24   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    26   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    25   val funpow: int -> ('a -> 'a) -> 'a -> 'a
    27   val funpow: int -> ('a -> 'a) -> 'a -> 'a
       
    28   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
       
    29   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    26 
    30 
    27   (*stamps*)
    31   (*stamps*)
    28   type stamp
    32   type stamp
    29   val stamp: unit -> stamp
    33   val stamp: unit -> stamp
    30 
    34 
   266 fun funpow n f x =
   270 fun funpow n f x =
   267   let fun rep (0, x) = x
   271   let fun rep (0, x) = x
   268         | rep (n, x) = rep (n - 1, f x)
   272         | rep (n, x) = rep (n - 1, f x)
   269   in rep (n, x) end;
   273   in rep (n, x) end;
   270 
   274 
       
   275 (*concatenation: 2 and 3 args*)
       
   276 fun (f oo g) x y = f (g x y);
       
   277 fun (f ooo g) x y z = f (g x y z);
   271 
   278 
   272 
   279 
   273 (** stamps **)
   280 (** stamps **)
   274 
   281 
   275 type stamp = unit ref;
   282 type stamp = unit ref;