CONJUNCTS_THEN : thm_tactical
STRUCTURE
Thm_cont
SYNOPSIS
Applies a theorem-tactic to each conjunct of a theorem.
DESCRIPTION
CONJUNCTS_THEN takes a theorem-tactic f, and a theorem t whose conclusion must be a conjunction. CONJUNCTS_THEN breaks t into two new theorems, t1 and t2 which are CONJUNCT1 and CONJUNCT2 of t respectively, and then returns a new tactic: f t1 THEN f t2. That is, 
   CONJUNCTS_THEN f (A |- l /\ r) =  f (A |- l) THEN f (A |- r)
so if 
   A1 ?- t1                    A2 ?- t2
  ==========  f (A |- l)      ==========  f (A |- r)
   A2 ?- t2                    A3 ?- t3
then 
    A1 ?- t1
   ==========  CONJUNCTS_THEN f (A |- l /\ r)
    A3 ?- t3

FAILURE
CONJUNCTS_THEN f will fail if applied to a theorem whose conclusion is not a conjunction.
COMMENTS
CONJUNCTS_THEN f (A |- u1 /\ ... /\ un) results in the tactic: 
   f (A |- u1) THEN f (A |- u2 /\ ... /\ un)
Unfortunately, it is more likely that the user had wanted the tactic: 
   f (A |- u1) THEN ... THEN f(A |- un)
Such a tactic could be defined as follows: 
   fun CONJUNCTS_THENL (f:thm_tactic) thm =
     List.foldl (op THEN) ALL_TAC (map f (CONJUNCTS thm));
or by using REPEAT_TCL.
SEEALSO
CONJUNCT1, CONJUNCT2, CONJUNCTS, CONJ_TAC, CONJUNCTS_THEN2, STRIP_THM_THEN
HOL  Kananaskis-11