NUM_REL_CONV : term -> thm
# NUM_REL_CONV `1089 < 2231`;; val it : thm = |- 1089 < 2231 <=> T # NUM_REL_CONV `1089 >= 2231`;; val it : thm = |- 1089 >= 2231 <=> F
# NUM_REL_CONV `2 + 2 = 4`;; Exception: Failure "REWRITES_CONV". # NUM_REDUCE_CONV `2 + 2 = 4`;; val it : thm = |- 2 + 2 = 4 <=> T