BODY_CONJUNCTS : (thm -> thm list)
STRUCTURE
Drule
SYNOPSIS
Splits up conjuncts recursively, stripping away universal quantifiers.
DESCRIPTION
When applied to a theorem, BODY_CONJUNCTS recursively strips off universal quantifiers by specialization, and breaks conjunctions into a list of conjuncts. 
    A |- !x1...xn. t1 /\ (!y1...ym. t2 /\ t3) /\ ...
   --------------------------------------------------  BODY_CONJUNCTS
          [A |- t1, A |- t2, A |- t3, ...]

FAILURE
Never fails, but has no effect if there are no top-level universal quantifiers or conjuncts.
EXAMPLE
The following illustrates how a typical term will be split: 
   - local val tm = Parser.term_parser
                        `!x:bool. A /\ (B \/ (C /\ D)) /\ ((!y:bool. E) /\ F)`
     in
     val x = ASSUME tm
     end;

     val x = . |- !x. A /\ (B \/ C /\ D) /\ (!y. E) /\ F : thm

   - BODY_CONJUNCTS x;
   val it = [. |- A, . |- B \/ C /\ D, . |- E, . |- F] : thm list

SEEALSO
CONJ, CONJUNCT1, CONJUNCT2, CONJUNCTS, CONJ_TAC
HOL  Kananaskis-14