DISCH_THEN : thm_tactic -> tactic
DISCH_THEN ttac (asl ?- t1 ==> t2) = ttac (ASSUME `t1`) (asl ?- t2)
A ?- t ======== ttac (ASSUME `u`) B ?- v
A ?- u ==> t ============== DISCH_THEN ttac B ?- v
# g `!x. x = 0 ==> f(x) * x = x + 2 * x`;;
# e(GEN_TAC THEN DISCH_THEN SUBST1_TAC);; val it : goalstack = 1 subgoal (1 total) `f 0 * 0 = 0 + 2 * 0`