U : ''a list list -> ''a list
STRUCTURE
Lib
SYNOPSIS
Takes the union of a list of sets.
DESCRIPTION
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
op_U, union, mk_set, mem, insert, set_eq, intersect, set_diff
HOL  Kananaskis-14