1\DOC U
2
3\TYPE {U : ''a list list -> ''a list}
4
5\SYNOPSIS
6Takes the union of a list of sets.
7
8\KEYWORDS
9list, set, eqtype.
10
11\DESCRIBE
12An application {U [l1, ..., ln]} is equivalent to
13{union l1 (... (union ln-1, ln)...)}. Thus, every element that
14occurs in one of the lists will appear in the result.
15
16\FAILURE
17Never fails.
18
19\EXAMPLE
20{
21- U [[1,2,3], [4,5,6], [1,2,5]];
22> val it = [3, 6, 4, 1, 2, 5] : int list
23}
24
25
26\COMMENTS
27The order in which the elements occur in the resulting list should
28not be depended upon.
29
30A high-performance implementation of finite sets may be found in
31structure {HOLset}.
32
33ML equality types are used in the implementation of {U} and its kin.
34This limits its applicability to types that allow equality. For other
35types, typically abstract ones, use the `op_' variants.
36
37\SEEALSO
38Lib.op_U, Lib.union, Lib.mk_set, Lib.mem, Lib.insert, Lib.set_eq, Lib.intersect, Lib.set_diff.
39\ENDDOC
40