POP_LAST_ASSUM : thm_tactic -> tactic
STRUCTURE
Tactical
SYNOPSIS
Applies tactic generated from the last element of a goal’s assumption list.
DESCRIPTION
When applied to a theorem-tactic and a goal, POP_LAST_ASSUM applies the theorem-tactic to the ASSUMEd last element of the assumption list, and applies the resulting tactic to the goal without that assumption in its assumption list: 
   POP_LAST_ASSUM f ({A1,...,Am,An} ?- t) = f (An |- An) ({A1,...,Am} ?- t)

FAILURE
Fails if the assumption list of the goal is empty, or the theorem-tactic fails when applied to the popped assumption, or if the resulting tactic fails when applied to the goal (with depleted assumption list).
COMMENTS
The tactical POP_LAST_ASSUM is also available under the lower-case version of the name, pop_last_assum.
SEEALSO
ASSUM_LIST, EVERY_ASSUM, IMP_RES_TAC, POP_ASSUM, REWRITE_TAC
HOL  Trindemossen-1