CONJ_PAIR
Drule.CONJ_PAIR : thm -> thm * thm
Extracts both conjuncts of a conjunction.
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.
See also
Drule.BODY_CONJUNCTS,
Thm.CONJUNCT1, Thm.CONJUNCT2,
Thm.CONJ, Drule.LIST_CONJ,
Drule.CONJ_LIST,
Drule.CONJUNCTS