1\DOC 2 3\TYPE {op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list} 4 5\SYNOPSIS 6Computes the union of two `sets'. 7 8\KEYWORDS 9list, set. 10 11\DESCRIBE 12If {l1} and {l2} are both `sets' (lists with no repeated members), 13{union eq l1 l2} returns the set union of {l1} and {l2}, using {eq} as the 14implementation of element equality. If one or both of {l1} and {l2} have 15repeated elements, there may be repeated elements in the result. 16 17\FAILURE 18If some application of {eq} fails. 19 20\EXAMPLE 21{ 22- op_union (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [5,4,7]; 23> val it = [5, 4, 7] : int list 24} 25 26 27\COMMENTS 28Do not make the assumption that the order of items in the list 29returned by {op_union} is fixed. Later implementations may use 30different algorithms, and return a different concrete result 31while still meeting the specification. 32 33There is no requirement that {eq} be recognizable as a kind of 34equality (it could be implemented by an order relation, for example). 35 36A high-performance implementation of finite sets may be found in 37structure {HOLset}. 38 39\SEEALSO 40Lib.union, Lib.op_mem, Lib.op_insert, Lib.op_mk_set, Lib.op_U, Lib.op_intersect, Lib.op_set_diff. 41\ENDDOC 42