export filter;
authorwenzelm
Tue May 31 11:53:20 2005 +0200 (2005-05-31)
changeset 161296fa9ace50240
parent 16128 927627fafca5
child 16130 38b111451155
export filter;
remove: generalized type;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue May 31 11:53:19 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 31 11:53:20 2005 +0200
     1.3 @@ -105,6 +105,7 @@
     1.4    val replicate: int -> 'a -> 'a list
     1.5    val multiply: 'a list * 'a list list -> 'a list list
     1.6    val product: 'a list -> 'b list -> ('a * 'b) list
     1.7 +  val filter: ('a -> bool) -> 'a list -> 'a list
     1.8    val filter_out: ('a -> bool) -> 'a list -> 'a list
     1.9    val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
    1.10    val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.11 @@ -179,7 +180,7 @@
    1.12    val ins_string: string * string list -> string list
    1.13    val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
    1.14    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.15 -  val remove: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.16 +  val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.17    val union: ''a list * ''a list -> ''a list
    1.18    val union_int: int list * int list -> int list
    1.19    val union_string: string list * string list -> string list
    1.20 @@ -274,7 +275,6 @@
    1.21    val flat: 'a list list -> 'a list
    1.22    val seq: ('a -> unit) -> 'a list -> unit
    1.23    val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.24 -  val filter: ('a -> bool) -> 'a list -> 'a list
    1.25    val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
    1.26  end;
    1.27