CONJ_PAIR : thm -> thm * thm
STRUCTURE
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
Fails if the input theorem is not a conjunction.
SEEALSO
HOL  Kananaskis-13