ind : hol_type
STRUCTURE
Type
SYNOPSIS
Basic type constant.
LIBRARY
Type
DESCRIPTION
The ML variable
Type.ind
is bound to the HOL type constant
ind
. The axiom
INFINITY_AX
in
boolTheory
states that
ind
represents an infinite set of individuals.
SEEALSO
bool
,
-->
HOL
Kananaskis-13