select : term
STRUCTURE
SYNOPSIS
Constant denoting Hilbert’s choice operator.
LIBRARY
boolSyntax
DESCRIPTION
The ML variable boolSyntax.select is bound to the term min$@.
SEEALSO
HOL  Kananaskis-13