NUM_RED_CONV : term -> thm
# NUM_RED_CONV `2 + 2`;; val it : thm = |- 2 + 2 = 4 # NUM_RED_CONV `1089 < 2231`;; val it : thm = |- 1089 < 2231 <=> T # NUM_RED_CONV `FACT 11`;; val it : thm = |- FACT 11 = 39916800
# NUM_RED_CONV `(432 - 234) + 198`;; Exception: Failure "REWRITES_CONV". # NUM_REDUCE_CONV `(432 - 234) + 198`;; val it : thm = |- 432 - 234 + 198 = 396
# let NUM_REDUCE_CONV' = DEPTH_CONV(REAL_RAT_RED_CONV ORELSEC conv);;