\DOC U

\TYPE {U : ''a list list -> ''a list}

\SYNOPSIS
Takes the union of a list of sets.

\KEYWORDS
list, set, eqtype.

\DESCRIBE
An application {U [l1, ..., ln]} is equivalent to
{union l1 (... (union ln-1, ln)...)}. Thus, every element that
occurs in one of the lists will appear in the result.

\FAILURE
Never fails.

\EXAMPLE
{
- U [[1,2,3], [4,5,6], [1,2,5]];
> val it = [3, 6, 4, 1, 2, 5] : int list
}


\COMMENTS
The order in which the elements occur in the resulting list should
not be depended upon.

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

ML equality types are used in the implementation of {U} and its kin.
This limits its applicability to types that allow equality. For other
types, typically abstract ones, use the `op_' variants.

\SEEALSO
Lib.op_U, Lib.union, Lib.mk_set, Lib.mem, Lib.insert, Lib.set_eq, Lib.intersect, Lib.set_diff.
\ENDDOC