CACHE_CONV : (term -> thm) -> term -> thm
# time (DEPTH_CONV NUM_RED_CONV) `31 EXP 31 + 31 EXP 31 + 31 EXP 31`;; CPU time (user): 1.542 val it : thm = |- 31 EXP 31 + 31 EXP 31 + 31 EXP 31 = 51207522392169707875831929087177944268134203293
# time (DEPTH_CONV(CACHE_CONV NUM_RED_CONV)) `31 EXP 31 + 31 EXP 31 + 31 EXP 31`;; CPU time (user): 0.461 val it : thm = |- 31 EXP 31 + 31 EXP 31 + 31 EXP 31 = 51207522392169707875831929087177944268134203293