TOP_DEPTH_CONV : conv -> conv
# TOP_DEPTH_CONV BETA_CONV `(\x. (\y. (\z. z + y) (y + 1)) (x + 2)) 3`;; val it : thm = |- (\x. (\y. (\z. z + y) (y + 1)) (x + 2)) 3 = ((3 + 2) + 1) + 3 + 2
# let conv = GEN_REWRITE_CONV I [MULT_CLAUSES] ORELSEC NUM_RED_CONV;; val conv : conv =# time (TOP_DEPTH_CONV conv) `0 * 25 EXP 100`;; CPU time (user): 0. val it : thm = |- 0 * 25 EXP 100 = 0
# time (REDEPTH_CONV conv) `0 * 25 EXP 100`;; CPU time (user): 2.573 val it : thm = |- 0 * 25 EXP 100 = 0