implement abbrevation tactics for subterms.

Fix bugs in Q's match_{rename,abbrev} tactics; refine spec.

In particular, make sure that instantiations arising from the matches
are applied in an order that is sure to make the substitutions apply
as much as possible. There are two obvious ways in which things can
go wrong (resulting in a goal-term that doesn't in fact look like the
supplied pattern).

1. If the match results in an instantiation that has a variable
binding a term that appears within another. E.g., (example from
Ramana):

Q.MATCH_RENAME_TAC `f v = z` (?- `f (h s) = s`)

The match will return (v |-> h s, z |-> s), but if this is applied
with the z going first, the goal won't contain `h s` when the
substitution for v is attempted. So that's bad, and affects both
renaming and abbreviating tactics.

The fix is to sort the instantiation list so that larger terms are
substituted out first.

2. Distinct variables in the pattern may end up binding the same
term. This is something users are less likely to bring about, but
it still seems worth trying to nail down what the behaviour should
be. E.g.,

Q.MATCH_RENAME_TAC `a + b = 10` (?- 5 + 5 = 10)

This will want to bind a and b to 5. When abbreviating, you might
like to see abbreviations `a = 5` and `b = 5` in the assumptions,
and when renaming or abbreviating, you might like to have the goal
become `a + b = 10`. Achieving both these might be possible, but
seems hard. Instead, the operational approach of performing
substitutions in a sequence is stuck to, but the substitution is
sorted so that the variable with the earlier name goes first. This
means you'll get ?- a + a = 10 as the goal, and when abbreviating,
you'll get `a = b` and `b = 5` as abbreviations in the
assumptions.

The fixes in examples/ are generally because proofs have relied on
abbreviations *not* occurring, despite the presence of variables in
the pattern. The situation is analogous to the situation in 1. above,
where the user has exploited the fact that a binding hasn't been
introduced for v.

Implement a simple tactic to undo Abbrev in assumptions.

Suggested by Magnus, this tactic turns all assumptions of the form
Abbrev (t1 = t2)
into
t2 = t1

Added MATCH_ASSUM_ABBREV_TAC to Q and markerLib.

This completes the set of pattern-matching tactics spanning the two dimensions of abbreviate/rename and conclusion/assumptions.

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.

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

A little code reorganisation and a fix for a bug in the implementation
of ASM_SIMP_TAC and FULL_SIMP_TAC: abbreviation references in the
argument list weren't being dealt with early enough. In the case of
ASM_SIMP_TAC this caused the effect of an abbreviation being eliminated
in the assumptions but not in the goal.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Support for rewriting annotations.

Moved marker stuff to its own directory, and also used same_const
function in new markerLib.
In a far off, distant land, where we implement named assumptions using
Konrad's NAMED constant (see src/basicProof/Notes), this stuff will
need to put back into bool so that the basic tactics can be made to work
with named assumptions.