\DOC CONJUNCT2

\TYPE {CONJUNCT2 : thm -> thm}

\SYNOPSIS
Extracts right conjunct of theorem.

\KEYWORDS
rule, conjunction.

\DESCRIBE
{
    A |- t1 /\ t2
   ---------------  CONJUNCT2
       A |- t2
}


\FAILURE
Fails unless the input theorem is a conjunction.

\COMMENTS
The theorem {AND2_THM} can be instantiated to similar effect.

\SEEALSO
Drule.BODY_CONJUNCTS, Thm.CONJUNCT1, Drule.CONJ_PAIR, Thm.CONJ, Drule.LIST_CONJ, Drule.CONJ_LIST, Drule.CONJUNCTS.
\ENDDOC