Make wordsLib.word_EQ_CONV and stringLib.string_EQ_CONV slightly more efficient.

Also extend the coverage of some *Syntax structures.

Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence.

Includes some tidying-up work.

This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib.

This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.

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!

Add syntax functions for div2 and mod_2exp.

Add reduction of DIV2 and MOD_2EXP to num compset and standard simpsets.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Reorganization of numSimps.sml (it was a bit of a jumble). Also,
added MIN and MAX syntax functions.

Some syntax operations added for WF relations. Also, a change to
recInduct, which wasn't doing what it should. I haven't tested
this mcuh, so any errors found, please send to me!

Added more support for prettyprinting numerals and parsing them.
src/theoryML/numML will now deal with binary, octal, decimal, and
hex.

Added DIVMOD to arithmeticScript, which helps complete the suite
of generated code. Unfortunately, arithmetic then depends on pairs,
which I had been trying to avoid, for purely aesthetic reasons.

Also fixed up more of the ML code generation business.

Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively.
Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.

Support for ML evaluation of numbers. Temporary.

Many small changes, most associated with boolification or lifting.

Added type abbreviations for bags (
Added type abbreviations ('a bag, 'a multiset) to bagTheory. Minor
supplements to existing syntax APIs. Fixed a bug in listSyntax.dest_list,
found by Peter Homeier.

Minor improvements and bugfixes.

Added numSyntax library. Very incomplete for now.