HYP : (thm list -> tactic) -> string -> thm list -> tactic
# g `p /\ q /\ r ==> r /\ q`;;
# e(INTRO_TAC "asm_p asm_q asm_r");; val it : goalstack = 1 subgoal (1 total) 0 [`p`] (asm_p) 1 [`q`] (asm_q) 2 [`r`] (asm_r) `r /\ q`
# e(HYP MESON_TAC "asm_r asm_q" []);; val it : goalstack = No subgoals