CONJ : thm -> thm -> thm
STRUCTURE
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
HOL  Kananaskis-13