NUM_MULT_CONV : term -> thm
|- n * m = s
# NUM_MULT_CONV `12345 * 12345`;; val it : thm = |- 12345 * 12345 = 152399025