LIST_CONJ
Drule.LIST_CONJ : thm list -> thm
Conjoins the conclusions of a list of theorems.
A1 |- t1 ... An |- tn
---------------------------------- LIST_CONJ
A1 u ... u An |- t1 /\ ... /\ tn
Failure
LIST_CONJ fails if applied to an empty list of theorems.
See also
Drule.BODY_CONJUNCTS,
Thm.CONJ, Thm.CONJUNCT1,
Thm.CONJUNCT2,
Drule.CONJUNCTS,
Drule.CONJ_PAIR,
Tactic.CONJ_TAC