Replace :label with :ind

There is no real need for a new type here.

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

map marker$stmarker to Unwanted.id

add opentheory name for marker$AC

Currently using Data.Bool./\\, but it might make sense to use a HOL4
specific name for this... we'll see.

add various names to the OpenTheory map

This is in preparation for logging llistTheory.

Notes:
- Sent combin$C to Function.Combinator.c (same for combin$S).
Another name might be preferred on the OpenTheory side.
- Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace.
- Put lots of pred_set constants in the Set namespace, but in the
standard (OpenTheory) library it seems like Set is for constants
operating on an abstract type of sets (rather than predicates). I'm
not sure whether we should use a different namespace when working with
sets-as-predicates or just pretend predicates are the abstract type
and do a bit of magic on article reading/writing as necessary (don't
know what that would be exactly yet).
- Similar for constants in set_relation, which I'm currently putting in
the Relation namespace. Although it looks like currently OpenTheory
doesn't use an abstract type of relations (but probably it will
later).
- Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if
Unwanted.id is supposed to be polymorphic (whereas those are identity
functions restricted to bool). Similar for numeral$iZ
- sent GSPEC to Set.specification; maybe not an obvious name...
- Using top-level "While" namespace for whileTheory
- dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it
- BIT2 is going to Number.Numeral.bit2; this is in line with wanting the
base library to be liberal, i.e. a union of all useful basic constants
and theorems (so has bit0, bit1 and bit2)... but I think there may be
competing goals for base

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.

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

Remove cutesy parsing hack from Abbrevs. May implement something in
the goal-stack pretty-printer to emulate this.

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.

Numerous minor changes associated with various things, most having
to do with exporting ML.

Support for rewriting annotations.

Provide an unint "tag" constant for use elsewhere in the system.

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.