1\DOC set_diff 2 3\TYPE {set_diff : ''a list -> ''a list -> ''a list} 4 5\SYNOPSIS 6Computes the set-theoretic difference of two `sets'. 7 8\KEYWORDS 9list, set, eqtype. 10 11\DESCRIBE 12{set_diff l1 l2} returns a list consisting of those elements of {l1} that do 13not appear in {l2}. It is identical to {Lib.subtract}. 14 15\FAILURE 16Never fails. 17 18\EXAMPLE 19{ 20- set_diff [] [1,2]; 21> val it = [] : int list 22 23- set_diff [1,2,3] [2,1]; 24> val it = [3] : int list 25} 26 27 28\COMMENTS 29The order in which the elements occur in the resulting list should 30not be depended upon. 31 32A high-performance implementation of finite sets may be found in 33structure {HOLset}. 34 35ML equality types are used in the implementation of {union} and its kin. 36This limits its applicability to types that allow equality. For other 37types, typically abstract ones, use the `op_' variants. 38 39\SEEALSO 40Lib.op_set_diff, Lib.subtract, Lib.mk_set, Lib.set_eq, Lib.union, Lib.intersect. 41\ENDDOC 42