1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC CONJ_PAIR
\TYPE {CONJ_PAIR : thm -> thm * thm}
\SYNOPSIS
Extracts both conjuncts of a conjunction.
\KEYWORDS
rule, conjunction.
\DESCRIBE
{
A |- t1 /\ t2
---------------------- CONJ_PAIR
A |- t1 A |- t2
}
\noindent The two resultant theorems are returned as a pair.
\FAILURE
Fails if the input theorem is not a conjunction.
\EXAMPLE
{
# CONJ_PAIR(ASSUME `p /\ q`);;
val it : thm * thm = (p /\ q |- p, p /\ q |- q)
}
\SEEALSO
CONJUNCT1, CONJUNCT2, CONJ, CONJUNCTS.
\ENDDOC
|
