Maps a string of numbers to the corresponding integer.
DESCRIBE
Found in the hol88 library. Given a string representing an integer in
standard decimal notation, possibly including a leading plus sign or
minus sign and/or leading zeros, int_of_string returns the
corresponding integer constant.
FAILURE
Fails unless the string is a valid decimal representation as specified
above. It will not be found unless the hol88 library has been loaded.
COMMENTS
Not found in hol90, since the author always got it backwards; use
string_to_int instead. Likewise, string_of_int is not found in hol90; use
int_to_string.