CONJUNCTS : thm -> thm list

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 CONDITIONS
Never fails.

EXAMPLE
  # CONJUNCTS(ASSUME `(x /\ y) /\ z /\ w`);;
  val it : thm list =
    [(x /\ y) /\ z /\ w |- x; (x /\ y) /\ z /\ w |- y; (x /\ y) /\ z /\ w
     |- z; (x /\ y) /\ z /\ w |- w]

SEE ALSO
CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR.