fix bug in congLib

fix a bug introduced by the change of REDUCER interface
in 3af1cefc94914690ff91c70ec41fda103152bd56.

rename Ho_Net.empty_net to Ho_Net.empty

All similar structures (e.g. Net and Raw) use "empty" not "empty_net";
it seems right to follow a single naming convention.

Remove unnecessary abstype constructions in {simp,cong}Lib.

These just make debugging more painful than it needs to be.

Get congLib to compile again by changing Traverse API again.

Rewriters get access both to the term of the current relation and a
function that will give them an instance of reflexivity for that
relation. Thomas's code was using this possibility.

Generalise congruence API to handle terms with free vars as equivs.

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!

A check "thm_rel = preorder" in "cong_rewrite" has been replaced by "samerel thm_rel preorder". This allows the preorder in congruence rules to have different type instantiations.

Change relations that have congruence rules stored for them
(they have to be preorders) to be stored as terms rather than string
pairs (the latter encoded theory and term name, allowing constants
only). The samerel function is now what should be used to determine
if two preorders are compatible. The use of same_const and aconv
means that only single constants can be used polymorphically, but
arbitrary monomorphic terms can be used elsewhere. (It's possible
this breaks Thomas Türk's examples; I have run selftest 1 on
everything else.)

Implement a scheme whereby a simpset can be limited to apply no more
than a limited number of rewrites/conversions/d.p. invocations. The
limit is stored in a simpset. By default all simpsets are unlimited.
To limit a simpset, use
limit n simpset
and it will then stop simplifying after n actions.

There is a border case: if a conditional rewrite requires exactly as
many rewrites to solve its side-conditions as it is limited to, it
will still go through with the rewrite, thereby exceeding the limit by
one (n side conditions, plus the final simplification)

The design is there to give a (better) guarantee of termination than
simpLib currently provides. For this reason, I didn't go with the
otherwise appealing idea of just letting side-condition discharge
ignore the limit entirely.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Added some tactics, EQ-CONV and rules. Also fixed some bugs with adding context and optimised some things.

Uses the new interface of CONGPROC. Thereby, a bug that occured, when multiple congruence relations in a congruence rule are used, has been eliminated.

Initial revision