CONJ_PAIR : thm -> thm * thm

SYNOPSIS

Extracts both conjuncts of a conjunction.

DESCRIPTION

       A |- t1 /\ t2
   ----------------------  CONJ_PAIR
    A |- t1      A |- t2

The two resultant theorems are returned as a pair.

FAILURE CONDITIONS

Fails if the input theorem is not a conjunction.

EXAMPLE

  # CONJ_PAIR(ASSUME `p /\ q`);;
  val it : thm * thm = (p /\ q |- p, p /\ q |- q)

SEE ALSO

CONJUNCT1, CONJUNCT2, CONJ, CONJUNCTS.