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