set_diff
Lib.set_diff : ''a list -> ''a list -> ''a list
Computes the set-theoretic difference of two 'sets'.
set_diff l1 l2 returns a list consisting of those elements of l1
that do not appear in l2. It is identical to Lib.subtract.
Failure
Never fails.
Example
> set_diff [] [1,2];
val it = []: int list
> set_diff [1,2,3] [2,1];
val it = [3]: 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 union and its kin.
This limits its applicability to types that allow equality. For other
types, typically abstract ones, use the 'op_' variants.
See also
Lib.op_set_diff, Lib.subtract,
Lib.mk_set, Lib.set_eq,
Lib.union, Lib.intersect