report_timing : bool ref
# time NUM_REDUCE_CONV `2 EXP 300 < 2 EXP 200`;; CPU time (user): 0.13 val it : thm = |- 2 EXP 300 < 2 EXP 200 <=> F # report_timing := false;; val it : unit = () # time NUM_REDUCE_CONV `2 EXP 300 < 2 EXP 200`;; val it : thm = |- 2 EXP 300 < 2 EXP 200 <=> F