strengthen holSemantics.proves_IMP

add Const n (typeof t) to deftm (Constdef n t); this gives a somewhat
quick route to showing that defined constants in an ok context are
term_ok. (not sure if such a route didn't already exist.)
prove another hol_verificationScript.sml cheat
use capital A type variable for Equal/Select

to be consistent with the aty abbreviation defined in
hol_verificationScript.sml (and with the HOL Light convention...)
clean up header of hol_verificationScript.sml

make it nicer for vim mode and vim's (broken) syntax highlighting for
SML
prove another cheat in hol_verificationScript.sml
prove another cheat in hol_verificationScript.sml