update inference system to use alpha-order-sorted lists for hyps

The ordering is proved transitive and antisymmetric; incomparables are
ACONV. The inference system is proved to only produce sequents whose
hypothesis lists are sorted and all-distinct-upto-alpha.

holConservativeScript.sml and beyond are likely broken in this commit.
comment out most of holConservativeScript.sml

to be updated later
remove redundant aconv_distinct clause from hypset_ok

SORTED by alpha_lt already implies being distinct, since it's a
strict less-than relation.
fix soundness proof for updated inference system
move invert_def to comparisonTheory (in HOL)
update monadic functions and proof

to use the new approach to hypothesis lists
define mlstring_cmp from mlstring_lt
functional equations for type_cmp and term_cmp
possible induction theorems for type_cmp and term_cmp

not sure how careful the statement of these needs to be for the
translator...
start updating ml_hol_kernelScript.sml

got stuck with translating type_cmp and term_cmp because they recurse
through a higher-order function.
Some progress on conservativity script
ml_hol_kernel builds, definitions made suitable for ML
Merge remote-tracking branch 'origin/orda'