ind : hol_type
STRUCTURE
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
HOL  Kananaskis-13