An invocation is_numeral tm, where tm is a HOL term with
the following form
returns true; otherwise, false is returned.
The NUMERAL constant is used as a tag signalling that its argument
is indeed a numeric literal. The ZERO constant is equal to 0,
and BIT1(n) = 2*n + 1 while BIT2(n) = 2*n + 2. This representation
allows asymptotically efficient operations on numeric values.
<numeral> ::= 0 | NUMERAL <bits>
<bits> ::= ZERO | BIT1 (<bits>) | BIT2 (<bits>)
The system prettyprinter will print a numeral as a string of digits.