CONJUNCT2 : thm -> thm
STRUCTURE
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
HOL  Kananaskis-10