- 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.