1\DOC CONJUNCT2 2 3\TYPE {CONJUNCT2 : thm -> thm} 4 5\SYNOPSIS 6Extracts right conjunct of theorem. 7 8\KEYWORDS 9rule, conjunction. 10 11\DESCRIBE 12{ 13 A |- t1 /\ t2 14 --------------- CONJUNCT2 15 A |- t2 16} 17 18 19\FAILURE 20Fails unless the input theorem is a conjunction. 21 22\COMMENTS 23The theorem {AND2_THM} can be instantiated to similar effect. 24 25\SEEALSO 26Drule.BODY_CONJUNCTS, Thm.CONJUNCT1, Drule.CONJ_PAIR, Thm.CONJ, Drule.LIST_CONJ, Drule.CONJ_LIST, Drule.CONJUNCTS. 27\ENDDOC 28