/usr/share/hol88-2.02.19940316/help/ENTRIES/CONJUNCTS.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 34 35 | \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
Suppose the identifier {th} is bound to the theorem:
{
A |- (x /\ y) /\ z /\ w
}
\noindent Application of {CONJUNCTS} to {th} returns the following list of
theorems:
{
[A |- x; A |- y; A |- z; A |- w] : thm list
}
\SEEALSO
BODY_CONJUNCTS, CONJ_LIST, LIST_CONJ, CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR.
\ENDDOC
|