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

Compiles up to src/parse under Poly/ML

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

More assorted code tidying.

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

Implement more of Basis2002 for Moscow ML (adding Vector, Array,
ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate.
Haven't done full rebuild test, but have got as far as integerTheory
and Omega, which makes heavy uses of Vector etc.

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.

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.

Fix string-to-arbnum conversion problems.

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.

Added signature to Portable. Trivial changes to Arbnum.

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