mk_rewrites : bool -> thm -> thm list -> thm list
# 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)]