Allow interactive uses of Hol_datatype to emit warnings.

Our interactive preludes were turning warnings off within calls to
Hol_datatype. Konrad's commit doing this, 7839c3ab, doesn't explain
why and I think it's a bad idea (if Hol_datatype is too chatty, fix
Hol_datatype rather than hack the preludes).

Use CharVector.tabulate instead of String.implode o List.tabulate.

SingleStep gets pulled in by the interactive
initialization code. So deleted.

Modify the initialisation of interactive pretty-printing in Moscow ML
so that the code in std.prelude doesn't need to be duplicated in
end-init-boss.sml.

Don't really know what I'm doing but this gets an interactive session working
under Moscow ML.

Was getting:

[loading theories and proof tools *************** ]
File "/Users/acjf3/HOL/tools/end-init-boss.sml", line 33, characters 13-38:
! installPP (with_pp simpLib.pp_ssfrag);
! ^^^^^^^^^^^^^^^^^^^^^^^^^
! Type clash: expression of type
! ppstream/1 -> 'a -> unit
! cannot have type
! ppstream -> 'b -> unit

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!

Several changes in order to start making emitML a
bit more usable.

1. pred_setLib is now loaded by bossLib.

2. Many applications of emitML will just use
the "standard" background provided by the
ML code generated from the theories available
when bossLib is loaded: bools, funs, pairs,
sums, nums, lists, and sets. To access these,
you don't have to do anything other than just
load and/or open "emitLib". To load other
pre-built emitML support for theories like
words, bags, etc. which are not loaded by
bossLib, you have to explicitly load the relevant
"emit" theories, e.g.

words_emitTheory

3. src/emit/theories has now been lifted into
src/emit. So EmitML, emitLib, and all the
basic x_emitScript.sml stuff lives in the
same directory. This was just because I
didn't bother to figure out how (or if) it
is possible to compile part of emit then
enter and compile all of emit/theories,
then return and compile the rest of emit
which depends on the theories. If that
scenario is possible with the right Holmakefile,
then possibly the previous directory structure
should be restored.

4. The dependency of EmitML on integers has been
eliminated. So examples/ordinalScript.sml
builds again.

5. The reference cell EmitML.reshape_thm_hook can
be used to stick standard pre-processing for
theorems.

Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

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.

Update to EmitTeX. Some functions have been renamed and some help entries
have been added.

EmitTeX is no longer included in bossLib and is instead loaded using
end-init-boss.sml.

Added proofManagerLib. This adds a type of "goal trees"
as an alternative to goalstacks. Relevant entrypoints:

gt ` .... ` -- start a goaltree proof,
analogous to g
eq ` ... ` -- expand a tactic,
analogous to e (except that
the text of the tactic is
delimited by quotes).

A goaltree manages the construction of the final
tactic, so should ease some of the script maintenance
that the goalstack requires.

Backup and restart are just as for goalstacks.

All the entrypoints for goalstacks are just as they
were before; there shouldn't be any difference.

Fix for start-up fragility, where files in the
current directory could shadow files in sigobj.

Removed substTheory.

Moved the function substitution operation (:-) to standard part of
the distribution.

substTheory.SUBST_EVAL:
|- !f a b c. (a :- b) f c = (if a = c then b else f c)

A couple of theorems have been renamed in the process:

SUBST_EQ2 -> SUBST_IMP_ID
SUBST_EQ3 -> SUBST_ID

Likewise renamed these theorems for FCP substitution (:+).

We need a bit more space now.

Added n-bit to the build sequence.

Minor fiddling.

Moved loading of src/datatype/Interactive to end-init-boss.sml. Was
formerly in mangled std.prelude checkin.

Modifications to remove the need of std.prelude to be generated from the
std.prelude.src file. Also cleaned up the way the executables are
generated.

Change to the start-up behaviour of HOL. At configuration time
the following 4 scripts get placed in the bin directory (as well as
a few others, e.g., Holmake):

hol -- loads and opens bossLib
hol.bare -- loads and opens boolLib only
hol.unquote -- the hol script, input passed through quotation filter
hol.bare.unquote -- the hol.bare script, using quotation filter

Most of the time, the hol or hol.unquote scripts offer the "right" context
for people to start working in.

This is tentative: I may change the names of the scripts
(suggestions welcome), or increase the libraries that the
hol/hol.unquote scripts load and open by default.

config-muddy.sml has been incorporated into configure.sml