CONJUNCTS : (thm -> thm list)
STRUCTURE
Drule
SYNOPSIS
Recursively splits conjunctions into a list of conjuncts.
DESCRIPTION
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
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
HOL  Kananaskis-8