`mk_rewrites : bool -> thm -> thm list -> thm list`

SYNOPSIS
Turn theorem into list of (conditional) rewrites.

DESCRIPTION
Given a Boolean flag b, a theorem th and a list of theorems thl, the call mk_rewrites b th thl breaks th down into a collection of rewrites (for example, splitting conjunctions up into several sub-theorems) and appends them to the front of thl (which are normally theorems already processed in this way). Non-equational theorems |- p are converted to |- p <=> T. If the flag b is true, then implicational theorems |- p ==> s = t are used as conditional rewrites; otherwise they are converted to |- (p ==> s = t) <=> T. This function is applied inside extend_basic_rewrites and set_basic_rewrites.

FAILURE CONDITIONS
Never fails.

EXAMPLE
```  # ADD_CLAUSES;;
val it : thm =
|- (!n. 0 + n = n) /\
(!m. m + 0 = m) /\
(!m n. SUC m + n = SUC (m + n)) /\
(!m n. m + SUC n = SUC (m + n))

# mk_rewrites false ADD_CLAUSES [];;
val it : thm list =
[|- 0 + n = n; |- m + 0 = m; |- SUC m + n = SUC (m + n);
|- m + SUC n = SUC (m + n)]
```

SEE ALSO
extend_basic_rewrites, GEN_REWRITE_CONV, REWRITE_CONV, set_basic_rewrites, SIMP_CONV.