Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

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

Splitting Arbnum and Arbint to work around the dependency on HOLPP before
moving into the mosml and poly directories.

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Support pretty-printing with different bases.

Add compare to Arbnum.

* Added bitsLib - this can be used for evaluating the functions in bitsTheory.
* Added LOG2 (log base 2) to bitsTheory (it's introduced with new_specification).
* log2 has been added to Arbnum - this provides fast evaluation for LOG2.

Support for turning strings of differently based digits into numbers.

* Added documentation.
* The pretty printing is now more flexible (off by default).
* Also added the function SIGN_EXTEND to bitsTheory and have
included a few more theorems.

Rewrote both kernels to cope with Overflow in Time.toSeconds by instead
going via a real, and using Arbnum. Also simplified the thyid type in
Theory.sml so that the representation was a pair of nums rather than a
time value that was being converted into and out of.

Moved toHexString to Arbnum.

+ Removed unnecessary renaming of MOD_1 and DIV_1 to MOD1 and DIV1 in bitsTheory.

* Added exponentiation (pow) to Arbnum.

* Added n_bit/Arbnum_ext.sml which contains toHexString : Arbnum.num -> string .
I guess this function could be added to Arbnum?

* Few minor tweaks to some proofs.

* Added theorems SBIT_MULT and WORD_BITS_COMP_THM2.

Provide gcd for arbitrary precision natural numbers.

Many small changes, most associated with boolification or lifting.

Typesetting.

General cleanup in view of the fact that we now have the Standard Basis
library. Hol98 assumes the existence of this!