LAST_ASSUM : (thm_tactic -> tactic)
STRUCTURE
SYNOPSIS
Maps a theorem-tactic over the assumptions, in reverse order, applying first successful tactic.
DESCRIPTION
LAST_ASSUM behaves like FIRST_ASSUM, except that it goes through the list of assumptions in reverse order
SEEALSO
HOL  Kananaskis-13