ASSUME_CONJS : term -> thm
STRUCTURE
SYNOPSIS
Constructs a theorem proving a conjunction from its individual conjuncts
DESCRIPTION
Takes a term which should be a conjunction, and returns a theorem whose hypotheses are the individual conjuncts, and whose conclusion is the argument term, the conjunction.
FAILURE
Never fails.
EXAMPLE
ASSUME_CONJS (``t1 /\ t2 /\ ... /\ tn``) returns  [t1, t2, ..., tn] |- t1 /\ t2 /\ ... /\ tn 

To split up conjuncts in selected hypotheses hyps of a theorem th, use Lib.itlist (PROVE_HYP o ASSUME_CONJS) hyps th

SEEALSO
HOL  Kananaskis-13