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
32
33
|
\DOC CONJUNCTS
\TYPE {CONJUNCTS : thm -> thm list}
\SYNOPSIS
Recursively splits conjunctions into a list of conjuncts.
\KEYWORDS
rule, conjunction.
\DESCRIBE
Flattens out all conjuncts, regardless of grouping. Returns a singleton list
if the input theorem is not a conjunction.
{
A |- t1 /\ t2 /\ ... /\ tn
----------------------------------- CONJUNCTS
A |- t1 A |- t2 ... A |- tn
}
\FAILURE
Never fails.
\EXAMPLE
{
# CONJUNCTS(ASSUME `(x /\ y) /\ z /\ w`);;
val it : thm list =
[(x /\ y) /\ z /\ w |- x; (x /\ y) /\ z /\ w |- y; (x /\ y) /\ z /\ w
|- z; (x /\ y) /\ z /\ w |- w]
}
\SEEALSO
CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR.
\ENDDOC
|
