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