----------------------------------------------------------------------
LAST_X_ASSUM                                                (Tactical)
----------------------------------------------------------------------
LAST_X_ASSUM : thm_tactic -> tactic

SYNOPSIS
Maps a theorem-tactic over the assumptions, in reverse order,
applying first successful tactic 
and removing the assumption that gave rise to the successful tactic.

KEYWORDS
theorem-tactical, assumption.

DESCRIBE
{LAST_X_ASSUM} behaves like {FIRST_X_ASSUM}, 
except that it goes through the list of assumptions in reverse order

SEEALSO
Tactical.FIRST_X_ASSUM, Tactical.LAST_ASSUM.

----------------------------------------------------------------------