HYP_TAC : string -> (thm -> thm) -> tactic
# g `!s. ~(s = ) ==> (minimal n. n IN s) IN s`;; # e (INTRO_TAC "!s; s");; # e (HYP_TAC "s : @a. +" (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]));; val it : goalstack = 1 subgoal (1 total) `a IN s ==> (minimal n. n IN s) IN s`
# e (MESON_TAC[MINIMAL]);;
# g `!x. &0 < x ==> &0 <= inv x`;; # e (INTRO_TAC "!x; xgt");; # e (HYP_TAC "xgt -> xge" (MATCH_MP REAL_LT_IMP_LE));; val it : goalstack = 1 subgoal (1 total) 0 [`&0 < x`] (xgt) 1 [`&0 <= x`] (xge) `&0 <= inv x`
# e (HYP SIMP_TAC "xge" [REAL_LE_INV]);;