DENUMERAL : thm -> thm

SYNOPSIS
Remove instances of the NUMERAL constant from a theorem.

DESCRIPTION
The call DENUMERAL th removes from the conclusion of th any instances of the constant NUMERAL, used in the internal representation of numerals.

FAILURE CONDITIONS
Never fails.

USES
Only intended for users manipulating the internal structure of numerals.

SEE ALSO
NUM_REDUCE_CONV.