SIMP_CONV : thm list -> conv
# SIMP_CONV[SUB_ADD; ARITH_RULE `0 < n ==> 1 <= n`] `0 < n ==> (n - 1) + 1 = n + f(k + 1)`;; val it : thm = |- 0 < n ==> n - 1 + 1 = n + f (k + 1) <=> 0 < n ==> n = n + f (k + 1)
# REWRITE_CONV[ADD_AC] `(a + c + e) + ((b + a + d) + e):num`;; val it : thm = |- (a + c + e) + (b + a + d) + e = a + a + b + c + d + e + e