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