ASSUME_TAC : thm_tactic
A ?- t ============== ASSUME_TAC (A' |- u) A u {u} ?- t
# g `0 = x ==> f(2 * x) = f(x * f(x))`;;
# e(DISCH_THEN(ASSUME_TAC o SYM));; val it : goalstack = 1 subgoal (1 total) 0 [`x = 0`] `f (2 * x) = f (x * f x)`
# e(ASM_REWRITE_TAC[MULT_CLAUSES]);; val it : goalstack = No subgoals