LAST_ASSUM : (thm_tactic -> tactic)
STRUCTURE
Tactical
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
FIRST_ASSUM
,
LAST_X_ASSUM
HOL
Kananaskis-14