CONJUNCT2 : thm -> thm
STRUCTURE
Thm
SYNOPSIS
Extracts right conjunct of theorem.
DESCRIPTION
    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
BODY_CONJUNCTS, CONJUNCT1, CONJ_PAIR, CONJ, LIST_CONJ, CONJ_LIST, CONJUNCTS
HOL  Kananaskis-13