CONJ : thm -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Introduces a conjunction.
DESCRIPTION
    A1 |- t1      A2 |- t2
   ------------------------  CONJ
     A1 u A2 |- t1 /\ t2

FAILURE
Never fails.
COMMENTS
The theorem AND_INTRO_THM can be instantiated to similar effect.
SEEALSO
BODY_CONJUNCTS, CONJUNCT1, CONJUNCT2, CONJ_PAIR, LIST_CONJ, CONJ_LIST, CONJUNCTS
HOL  Trindemossen-1