LAST_X_ASSUM : thm_tactic -> tactic

- STRUCTURE
- 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.
- DESCRIPTION
- LAST_X_ASSUM behaves like FIRST_X_ASSUM, except that it goes through the list of assumptions in reverse order
- SEEALSO

HOL Kananaskis-13