Terms and types print interactively.

Thms ignore grammars; term grammars print badly

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.

Quick fix for build failure under Moscow ML caused by my changes yesterday.

Many small changes, most associated with boolification or lifting.

Added minimum and maximum functions for arbitrary precision integers.

Extended and revised so that the div/mod functions now correspond to
what is done in ML's standard basis library's Integer structure. In
particular, there is now div/mod and also quot/rem, whose behaviours
differ on negative arguments (div rounds down; quot rounds towards zero).

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