1\DOC BODY_CONJUNCTS
2
3\TYPE {BODY_CONJUNCTS : (thm -> thm list)}
4
5\SYNOPSIS
6Splits up conjuncts recursively, stripping away universal quantifiers.
7
8\KEYWORDS
9rule, conjunction.
10
11\DESCRIBE
12When applied to a theorem, {BODY_CONJUNCTS} recursively strips off universal
13quantifiers by specialization, and breaks conjunctions into a list of
14conjuncts.
15{
16    A |- !x1...xn. t1 /\ (!y1...ym. t2 /\ t3) /\ ...
17   --------------------------------------------------  BODY_CONJUNCTS
18          [A |- t1, A |- t2, A |- t3, ...]
19}
20
21
22\FAILURE
23Never fails, but has no effect if there are no top-level universal quantifiers
24or conjuncts.
25
26\EXAMPLE
27The following illustrates how a typical term will be split:
28{
29   - local val tm = Parser.term_parser
30                        `!x:bool. A /\ (B \/ (C /\ D)) /\ ((!y:bool. E) /\ F)`
31     in
32     val x = ASSUME tm
33     end;
34
35     val x = . |- !x. A /\ (B \/ C /\ D) /\ (!y. E) /\ F : thm
36
37   - BODY_CONJUNCTS x;
38   val it = [. |- A, . |- B \/ C /\ D, . |- E, . |- F] : thm list
39}
40
41
42\SEEALSO
43Thm.CONJ, Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJUNCTS, Tactic.CONJ_TAC.
44\ENDDOC
45