Maps an integer to the corresponding decimal string.
DESCRIBE
Found in the hol88 library. When given an integer, string_of_int
returns a string representing the number in standard decimal notation,
with a leading minus sign if the number is negative, and no leading
zeros.
FAILURE
Never fails. The function is not available unless the hol88 library has been
loaded.
COMMENTS
Not found in hol90, since the author always got it backwards; use
int_to_string instead. Likewise, int_of_string is not found in hol90; use
string_to_int.