more hol_verification

finish thm functions, and some miscellany. < 10 cheats left.