Change INDUCT_THEN to cope with more induction theorem shapes

In particular, it previously assumed that outermost universal
variables in assumptions that were implications were always of the
same type as the induction variable. E.g., in a binary tree induction
axiom, the branch IH would be

!t1 t2. P t1 /\ P t2 ==> !a. P (Nd a t1 t2)

(note how the !a is under the implication).

The magic done by INDUCT_THEN would then change the variables t1 and
t2 to match the name of the induction variable in the actual goal (one
would be primed). But if you have a snazzier principle with an IH such
as

!ts. (!t. MEM t ts ==> P t) ==> !fnm. P (Fn fnm ts)

the outermost variable (which has to be outermost), is not of the
"right" type.

The fix allows for this, and also copes if the fnm quantification
floats out to the top-level. This facility is only relevant if a
non-standard induction theorem is installed for a type (see previous
commit). The standard theorems generated by Datatype are shaped as
INDUCT_THEN required.

Fix bug in generation of case_eq theorem for 'a itself

Fix bug in prove_case_elim_thm

Test-case tweaks old bug, which was caused by conflicting names. If
the first constructor in the type was

C ty

and a later constructor was D (ty -> bool), then the code would end up
with a theorem of the form

x = D f /\ ... |- caseconst x f f1 f2

where the f in the hypotheses corresponded to the argument to the D,
and the f in the conclusion corresponded to the function passed to the
case-constant, taking a ty and returning (in this case) a bool. Then,
when CHOOSE tried to wrap an existential around the f in the
hypothesis, it would fail because we'd inadvertently identified two
variables that were supposed to be different.

Fix is to be even more paranoid about choice of variable names when
stripping the existentials arising in type's nchotomy theorem.

Bug was apparent in examples/lambda/typing/type_schemasScript.sml

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

Remove eqtype declaration for term type

New prove_case_eq_thm entrypoint for Prim_rec

Implement function to prove a case-constant elimination rewrite

Implement and document a new prove_case_rand_thm function in Prim_rec.

This will be the basis for a general tool that moves case-constants up
within a term and then eliminates them, subsuming, for example, the
functionality in boolSimps.COND_elim_ss, which does this but only for
the boolean case-constant (aka if-then-else).

Clean up code that relies on constant and theorem names for case constants.

Rather than code having to know that the constant is called
“type_CASE” and that its definition is stored in “type_case_def”, use
ML entrypoints in Prim_rec to abstract these details.

This is progress with github issue #97.

Start of project to flip argument order in case constants.

One scary (but probably optional) change is to do away with bool_case
constant because it is now identical to COND. This could be reversed,
but having two constants with exactly the same type and semantics does
seem silly. I think the parsing/pretty-printing behaviour can be made
sensible even in the face of this unification.

Prim_rec’s functions for defining case constants and proving case
congruence theorems have been adjusted appropriately.

This is relevant to Github issue #97.

Correct a minor typo in a comment in Prim_rec.sml

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Change src/bool to src/1 as a prelude to experimentation!