LAST_ASSUME_TAC
Tactic.LAST_ASSUME_TAC : thm_tactic
Adds an assumption to the top of the assumptions.
Given a theorem th of the form A' |- u, and a goal,
LAST_ASSUME_TAC th adds u to the assumptions of the goal.
A ?- t
============== LAST_ASSUME_TAC (A' |- u)
{u} u A ?- t
Note that unless A' is a subset of A, this tactic is invalid.
Failure
Never fails.
LAST_ASSUME_TAC is the naive way of manipulating assumptions
(i.e. without recourse to advanced tacticals); and it is useful for
enriching the assumption list with lemmas as a prelude to resolution
(RES_TAC, IMP_RES_TAC), rewriting with assumptions
(ASM_REWRITE_TAC and so on), and other operations involving
assumptions.