Ensure HOL4 works with fixed-width integers under Poly/ML.

Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this:

- The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int.
- The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure.
- The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.

Improve error reporting for the Arbnum string parsing functions.

Previously

Arbnum.fromHexString "g"

would raise Option and

Arbnum.fromHexString "ag"

would return 10. Now both fail with a "String not HEX" message.

Slight tuneup for Arbnum.isqrt.

Some basic evaluation support for square roots over ``:num`` and ``:real``. Also add syntax support for transcTheory.

Tidied up logrootScript.sml. The evaluation theorems for ``ROOT 2`` were present but they weren't being used.

Over the reals a conversion is used -- this will only work for rationals built from perfect squares. For example:

> EVAL ``sqrt (9 / 16)``
val it = |- sqrt (9 / 16) = 3 / 4: thm

More assorted code tidying.

Remove trailing whitespace in source files.

The PolyML version now uses PolyML's builin IntInf support. (This change
doesn't appear to speed up HOL, but it's nice to have anyway.)