CONJ_LIST : (int -> thm -> thm list)
STRUCTURE
Drule
SYNOPSIS
Extracts a list of conjuncts from a theorem (non-flattening version).
DESCRIPTION
CONJ_LIST is the proper inverse of LIST_CONJ. Unlike CONJUNCTS which recursively splits as many conjunctions as possible both to the left and to the right, CONJ_LIST splits the top-level conjunction and then splits (recursively) only the right conjunct. The integer argument is required because the term tn may itself be a conjunction. A list of n theorems is returned. 
    A |- t1 /\ (t2 /\ ( ... /\ tn)...)
   ------------------------------------  CONJ_LIST n (A |- t1 /\ ... /\ tn)
    A |- t1   A |- t2   ...   A |- tn

FAILURE
Fails if the integer argument (n) is less than one, or if the input theorem has less than n conjuncts.
EXAMPLE
Suppose the identifier th is bound to the theorem: 
   A |- (x /\ y) /\ z /\ w
Here are some applications of CONJ_LIST to th: 
   - CONJ_LIST 0 th;
   ! Uncaught exception:
   ! HOL_ERR

   - CONJ_LIST 1 th;
   > val it = [[A] |- (x /\ y) /\ z /\ w] : thm list

   - CONJ_LIST 2 th;
   > val it = [ [A] |- x /\ y,  [A] |- z /\ w] : thm list

   - CONJ_LIST 3 th;
   > val it = [ [A] |- x /\ y,  [A] |- z,  [A] |- w] : thm list

   - CONJ_LIST 4 th;
   ! Uncaught exception:
   ! HOL_ERR

SEEALSO
BODY_CONJUNCTS, LIST_CONJ, CONJUNCTS, CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR
HOL  Kananaskis-14