null_intersection : ''a list -> ''a list -> bool
STRUCTURE
Lib
SYNOPSIS
Tells if two lists have no common elements.
DESCRIPTION
An invocation null_intersection l1 l2 is equivalent to null(intersect l1 l2), but is more efficient in the case where the intersection is not empty.
FAILURE
Never fails.
EXAMPLE
- null_intersection [1,2,3,4] [5,6,7,8];
> val it = true : bool

- null_intersection [1,2,3,4] [8,5,3];
> val it = false : bool

COMMENTS
A high-performance implementation of finite sets may be found in structure HOLset.
SEEALSO
intersect, union, U, mk_set, mem, insert, set_eq, set_diff
HOL  Kananaskis-14