Up to hol.state0

Make goals p/print faster by being less pretty on big goals

In particular, make the pretty-printing backend be the "raw" terminal for
all but last subgoal when printing goals of more than a particular
size (specified in Goalstack.other_subgoals_pretty_limit trace). This
should be particularly helpful for emacs users because printing type
annotations over many pages of output can be a definite slow-down.

Strictly, this is thus a help for big subgoal lists rather than big
goals. If you have really huge individual goals that are printing
slowly, you will just have to set the backend manually (though remember
that M-h C-p toggles back and forth between the emacs and raw backends).

Also publish goal_size and gstk_size functions in the goalStack API.

added flatn command in proofManagerLib

in interactive proof, to flatten subgoal stack, so as to merge current list of
subgoals with previous level(s)

expand_list to interactively work on a list of subgoals

also Tactical.VALID_LT, to check that a list-tactical is valid
(expand_list checks validity, expand_listf doesn't)

also abbreviations elt, eall, eta, enth to apply (list-)tactic to subgoal(s)

SML whitespace cleanup

A new debugging tactic, print_tac, that prints the goal state.

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.