Add elim_Case rules

Case markers are meant to become assumptions of goals, so this
rewrite set eliminates markers that have ended up in the wrong
place.

Add Case marker constant to markerTheory

Yet another trivial constant. This one will appear in assumptions
in goals of a proof by induction or case distinction, and will
clarify which case the current goal is.

Attempt at better Abbrev protection

This in the face of simplification and the variable elimination done
by RW_TAC and friends. Core sequence, -t1 and some of -t2 builds (up
to category theory example).

Machinery for dynamically reverting to the old behaviours possible
through diminish_srw_ss and a trace variable.

This is work on github issue #800

Tweak 'using' to now handle unnamed monomorphic theorem arguments

Allow Induct_on & Cases_on to use different theorems with 'using'

The using function is infix on tactics; other tactics can grab 'using'
theorems if they want to try, using the markerLib.maybe_using
entrypoint.

Allow "local" attribute to be added to Type syntax

This generates a temp_type_abbrev/temp_type_abbrev_pp call underneath.
Document and use in a few src files.

Thanks to Magnus for the suggestion.

Implement Req0/ReqD forms to require simp rules to have been applied

Closes #680

Add Excl theorem form to exclude things from simplification

For example

simp[Excl "BETA_CONV"]

will stop the BETA_CONV conversion from firing.

This doesn't interact correctly with remove_ssfrags properly yet
because that function rebuilds a simpset from its constituent
fragments, and so will put back stuff that Excl has removed. The
remove_ssfrags implementation will change to simply remove those
things in the simpset that have come from given fragments (meaning
that simpsets will no longer need to store their originating fragments
at all).

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

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.