CONJUNCT1
Thm.CONJUNCT1 : thm -> thm
Extracts left conjunct of theorem.
A |- t1 /\ t2
--------------- CONJUNCT1
A |- t1
Failure
Fails unless the input theorem is a conjunction.
Comments
The theorem AND1_THM can be instantiated to similar effect.
See also
Drule.BODY_CONJUNCTS,
Thm.CONJUNCT2,
Drule.CONJ_PAIR, Thm.CONJ,
Drule.LIST_CONJ,
Drule.CONJ_LIST,
Drule.CONJUNCTS