CONJUNCT2 : thm -> thm

SYNOPSIS
Extracts right conjunct of theorem.

DESCRIPTION
    A |- t1 /\ t2
   ---------------  CONJUNCT2
       A |- t2

FAILURE CONDITIONS
Fails unless the input theorem is a conjunction.

EXAMPLE
  # CONJUNCT2(ASSUME `p /\ q`);;
  val it : thm = p /\ q |- q

SEE ALSO
CONJ_PAIR, CONJUNCT1, CONJ, CONJUNCTS.