GEN_VALIDATE(_LT) - flag for adding new subgoals in any event

GEN_VALIDATE false is like VALIDATE, but adds subgoals for the assumptions
of the theorem produced by the justification, regardless of whether they
are among the assumptions of the goal.  Advantage of this is that
GEN_VALIDATE false (ACCEPT_TAC th) produces predictable subgoals,
which may help in coding compound tactics
Merge pull request #217 from jeremydaw/trial

GEN_VALIDATE(_LT) - flag for adding new subgoals in any event
reuse cpn datatype from totoTheory in comparisonTheory

rather than creating an isomorphic new type.

balanced_mapScript.sml has apparently (but not actually) significant
changes because the proofs depend heavily on the order in which the
comparison datatype constructors are defined (inasmuch as it affects the
order of subgoals from cases/induction).
prove TotOrd implies good_cmp
delete trailing whitespace in examples/balanced_bst