eliminated some ref-matches

Remove TABs from src

Will also make selftest to check that they aren't introduced

Strongly reduce initial arguments of set_skip'd constants.
Makes strong reduction on record updates reduce values properly

support for understanding what is in (and what needs to be added to) a compset

New utility function to add contents of a "theorem set" to a compset.

Give computeLib.compset a pretty-printer, and install it in Poly HOL.

This is necessary to stop Poly/ML 5.3 from trying to print out huge values
such as computeLib.the_compset.

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!

Remove another Polyhash

Added functionality for deleting definitions from compsets.
Usual usage:

del_consts [c1, ..., cn];

Other related control is also possible.

Made a bunch of changes to the HOL source to make it more "Standard ML",
to make it easier to port to MLton.

For example:
+ Added lots of structure wrappers around miscellaneous .sml files.
+ The type of "before" is 'a * () -> 'a, not 'a * 'b -> 'a, as Moscow ML
currently thinks.
+ Added "val _ = " before random declarations.

A plea: if I'm ever going to succeed in porting HOL to MLton, could
people please stop using Polyhash. It's very useful, but there's
nothing like it in MLton (or indeed Standard ML). In theory I'm going
to have to change the (sometimes complicated) code to use Binarymap or
something like it, but in practice I'll only do that when there's
absolutely no other way.

Modifications so that when tyinfos are added to the global compset, their
simpls_of component is added. This component includes the distinctness,
one-one and case-definition theorems already, so these theorems don't need
to be individually included. In the old code, the case definition was
subjected to a call to lazyfy_thm, but this had no effect, so the new
code is equivalent. Old and new code alike are WRONG:
all arms of a case will be evaluated before a decision as to which to take
is made.
This doesn't happen with lists and numbers because they both get
special purpose case_compute theorems thrown into the compset. I will
be adding a bug report to document this.
Finally, the change in clauses.sml is to prevent rewrites from being
added that might loop (such a rewrite exists in every set of simplifications
for record types; it's of the general form !v. f v = f c). This rewrite
turns f with <| .. complete set of fields |> into
<| complete set of fields |>

Minor changes.

Made Define store its resulting equations in the compset in a persistent
manner.

Improved error message for add_thms.

More changes supporting the global compset.

Minor changes.

Upgrades ... changed the type to be "compset".

Changed name of rules module to compute_rules, because rules clashes
with Tfl's Rules module under Windows NT, where names are case-
insensitive.

Removed the ugly boolean of add_thms and from_list.
Use lazyfy_thm or strictify_thm instead.
Modified examples accordingly.

improved the set_skip facility: must specify the arity at which the
decision to stop reducing the arguments should be made.

Better error message when mk_rewrite fails (prints the faulty thm).

- New feature: it is possible to prevent the reduction of the arguments of
a constant when no rule could be applied. Useful to avoid looping when the
boolean of a conditional does not reduce to T or F.
- theorems that are not equalities are prepocessed with
|- ~t --> |- t = F and |- t --> |- t = T

abstracted the type of theorems
generalized the type of external conversions

better tail-recursive version (but more complicated)
conversions can be added to simpl. sets.

fixed bug with out of date constants

Last minor changes before implementing the tail-recursive version.
Added a doc file.

added eta-conversion and an interface for computeLib.

added directory src/compute (without explicit substitutions in the kernel)