HO_MATCH_MP_TAC documentation (and other minor fixes)

Documentation `HO_MATCH_MP_TAC` probably still needs to be reviewed by HOL expert. Once approved, #204 can be closed.