some optional sanity checks for the virtual machine
fixes for thm command
add a reader for hol_ctxt

in particular, it knows how to prove (some) axioms in that context
prove cheat in example1 by reading an OpenTheory article