----------------------------------------------------------------------
op_union                                                         (Lib)
----------------------------------------------------------------------
op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list

SYNOPSIS
Computes the union of two ‘sets’.

KEYWORDS
list, set.

DESCRIBE
If {l1} and {l2} are both ‘sets’ (lists with no repeated members),
{union eq l1 l2} returns the set union of {l1} and {l2}, using {eq} as the
implementation of element equality. If one or both of {l1} and {l2} have
repeated elements, there may be repeated elements in the result.

FAILURE
If some application of {eq} fails.

EXAMPLE

- op_union (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [5,4,7];
> val it = [5, 4, 7] : int list




COMMENTS
Do not make the assumption that the order of items in the list
returned by {op_union} is fixed. Later implementations may use
different algorithms, and return a different concrete result
while still meeting the specification.

There is no requirement that {eq} be recognizable as a kind of
equality (it could be implemented by an order relation, for example).

A high-performance implementation of finite sets may be found in
structure {HOLset}.

SEEALSO
Lib.union, Lib.op_mem, Lib.op_insert, Lib.op_mk_set, Lib.op_U,
Lib.op_intersect, Lib.op_set_diff.

----------------------------------------------------------------------