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.

Correct arithmeticTheory to work with flipped case constants.

Progress with #97.

dest_numeral fails with correct origin fields in the error record, no longer
exposing its implementation in terms of Literal.dest_numeral.

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!

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Add syntax functions for div2 and mod_2exp.

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

Upgrading EmitML to support records. Lots of associated changes
as well.

Tell the code generator in EmitML what a num literal is.

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.

Getting rid of HTML output on xTheory.sig files.

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!

Hacking around to get HTML symbols put in generated `Theory.sig'
files. Allows usual logic symbols (and some set theory symbols)
in the generated html files, see help/HOLindex.html after a
complete build of the system (examine a theory file).

Only symbol not currently dealt with properly is lambda. Also,
I thought I had emptyset sussed, but it stopped working for
some reason ... not a problem since "{}" works just as well,
and may be nicer.

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.

Upgrades to ML code generation. It now works for numerals, although
the results of a computation will be incomprehensible usually. Writing
a prettyprinter needs to be done.

Support for ML evaluation of numbers. Temporary.

Many small changes, most associated with boolification or lifting.

Didn't compile.

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.

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

Minor changes.

Minor improvements and bugfixes.

paired syntax.

Added numSyntax library. Very incomplete for now.