CONJ_LIST : (int -> thm -> thm list)
STRUCTURE
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
HOL  Kananaskis-14