IMP_RES_THEN : thm_tactical
IMP_RES_THEN ttac th (A ?- g)
MAP_EVERY (mapfilter ttac [... ; (Ai u {aj} |- vi) ; ...]) (A ?- g)
# g `!a n. a + n = a ==> !k. k - n = k`;;
# e(REPEAT GEN_TAC THEN DISCH_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`a + n = a`] `!k. k - n = k`
# let ADD_INV_0 = ARITH_RULE `!m n. m + n = m ==> n = 0`;;
# e(IMP_RES_THEN SUBST1_TAC ADD_INV_0);; val it : goalstack = 1 subgoal (1 total) 0 [`a + n = a`] `!k. k - 0 = k`