RULE_L_ASSUM_TAC : ((thm -> thm list) -> tactic)
STRUCTURE
Tactic
SYNOPSIS
Maps an inference rule, which produces a list of result theorems, over the assumptions of a goal.
DESCRIPTION
When applied to an inference rule f and a goal ({A1,...,An} ?- t), the RULE_L_ASSUM_TAC tactical applies the inference rule to each of the ASSUMEd assumptions to give a new goal. 
             {A1,...,An} ?- t
   ====================================  RULE_L_ASSUM_TAC f
    {f(A1 |- A1),...,f(An |- An)} ?- t
Here each f(Ai |- Ai) is a list of assumptions.
FAILURE
The application of RULE_L_ASSUM_TAC f to a goal fails iff f fails when applied to any of the assumptions of the goal.
COMMENTS
It does not matter if the goal has no assumptions, but in this case RULE_L_ASSUM_TAC has no effect.
EXAMPLE
With a goal 
g
------------------------------------
  0.  a /\ b
  1.  c
  2.  d /\ e /\ f

the tactic RULE_L_ASSUM_TAC CONJUNCTS gives the new goal 

g
------------------------------------
  0.  a
  1.  b
  2.  c
  3.  d
  4.  e
  5.  f

RULE_L_ASSUM_TAC can also be used to delete unwanted assumptions: let f ass = [ass] for an assumption which is to be kept, and f ass = [] for an assumption which is to be deleted.

SEEALSO
RULE_ASSUM_TAC, ASSUM_LIST, MAP_EVERY, MAP_FIRST, POP_ASSUM_LIST
HOL  Trindemossen-1