FIRST_ASSUM : (thm_tactic -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Maps a theorem-tactic over the assumptions, applying first successful tactic.
DESCRIPTION
The tactic 
   FIRST_ASSUM ttac ([A1; ...; An], g)
has the effect of applying the first tactic which can be produced by ttac from the ASSUMEd assumptions (A1 |- A1), ..., (An |- An) and which succeeds when applied to the goal. Failures of ttac to produce a tactic are ignored.
FAILURE
Fails if ttac (Ai |- Ai) fails for every assumption Ai, or if the assumption list is empty, or if all the tactics produced by ttac fail when applied to the goal.
EXAMPLE
The tactic 
   FIRST_ASSUM (fn asm => CONTR_TAC asm  ORELSE  ACCEPT_TAC asm)
searches the assumptions for either a contradiction or the desired conclusion. The tactic 
   FIRST_ASSUM MATCH_MP_TAC
searches the assumption list for an implication whose conclusion matches the goal, reducing the goal to the antecedent of the corresponding instance of this implication.
SEEALSO
FIRST_X_ASSUM, ASSUM_LIST, EVERY, EVERY_ASSUM, FIRST, MAP_EVERY, MAP_FIRST
HOL  Kananaskis-11