src/Pure/library.ML
changeset 26449 283107142592
parent 26439 e38f7e1c07ce
child 27850 49503146b853
     1.1 --- a/src/Pure/library.ML	Thu Mar 27 19:04:42 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 27 19:05:10 2008 +0100
     1.3 @@ -109,6 +109,8 @@
     1.4    val ~~ : 'a list * 'b list -> ('a * 'b) list
     1.5    val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
     1.6    val split_list: ('a * 'b) list -> 'a list * 'b list
     1.7 +  val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     1.8 +  val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.9    val separate: 'a -> 'a list -> 'a list
    1.10    val surround: 'a -> 'a list -> 'a list
    1.11    val replicate: int -> 'a -> 'a list
    1.12 @@ -158,8 +160,6 @@
    1.13    val replicate_string: int -> string -> string
    1.14    val translate_string: (string -> string) -> string -> string
    1.15    val multiply: 'a list -> 'a list list -> 'a list list
    1.16 -  val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.17 -  val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.18  
    1.19    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.20    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool