Started work on making the AST optionally typed.

I commented out several lemmas in MiniMLTerminationScript.sml having to
do with size functions that are no longer true.
new version of syntax.ml and generated .art-file
working version of HOL Light export and HOL4 import
inference now allow definitions
complete first draft of changes to John\'s syntax.ml
deleting old files
Rename Ref and Deref to Opref and Opderef
Complete the move to optionally type annotated terms.

The proofs in metatheory work (except for typeSoundScript.sml) but this
will undoutably break everything else because the AST changes.  Most are
minor.  The only possible concern in that the evaluate rule changes to:

forall cenv env n v s targs_opt type_scheme_opt.
(lookup n env = Some (v,type_scheme_opt))
==>
evaluate cenv s env (Var n targs_opt) (s, Rval (do_tapp type_scheme_opt targs_opt v))

if either of the optional things are None, then do_tapp returns v, but
if they are both annotated, then do_tapp does a substitution in v of
targs for the type variables bound in type scheme.  This substitution
only affects annotations in v.
Some progress toward fixing the type soundness proof.
Support for axioms added and general progress...
Merge branch 'master' of github.com:xrchz/vml
Fix to build with latest HOL with the new case argument ordering.
More progress on type soundness
fixed a borken proof, cheated on another
a bit of progress on getting the translator building again, deBruijn indexes are getting in the way
translator works again, but with NONE everywhere
Fix cheat
More progress on type soundness.
More progress on type soundness
progress towards translation of monadic functions