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