set_diff : ''a list -> ''a list -> ''a list
STRUCTURE
Lib
SYNOPSIS
Computes the set-theoretic difference of two ‘sets’.
DESCRIPTION
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.

SEEALSO
op_set_diff, subtract, mk_set, set_eq, union, intersect
HOL  Kananaskis-13