DISJ_CASES_THENL : (thm_tactic list -> thm_tactic)
STRUCTURE
SYNOPSIS
Applies theorem-tactics in a list to the corresponding disjuncts in a theorem.
DESCRIPTION
If the theorem-tactics f1...fn applied to the ASSUMEd disjuncts of a theorem
   |- d1 \/ d2 \/...\/ dn
produce results as follows when applied to a goal (A ?- t):
    A ?- t                                A ?- t
   =========  f1 (d1 |- d1) and ... and =========  fn (dn |- dn)
    A ?- t1                              A ?- tn
then applying DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn) to the goal (A ?- t) produces n subgoals.
           A ?- t
   =======================  DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn)
    A ?- t1  ...  A ?- tn
DISJ_CASES_THENL is defined using iteration, hence for theorems with more than n disjuncts, dn would itself be disjunctive.
FAILURE
Fails if the number of tactic generating functions in the list exceeds the number of disjuncts in the theorem. An invalid tactic is produced if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.
USES
Used when the goal is to be split into several cases, where a different tactic-generating function is to be applied to each case.
SEEALSO
HOL  Kananaskis-14