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.