NUM_EXP_CONV : term -> thm
|- n EXP m = s
# NUM_EXP_CONV `2 EXP 64`;; val it : thm = |- 2 EXP 64 = 18446744073709551616 # NUM_EXP_CONV `1 EXP 99`;; val it : thm = |- 1 EXP 99 = 1 # NUM_EXP_CONV `0 EXP 0`;; val it : thm = |- 0 EXP 0 = 1 # NUM_EXP_CONV `0 EXP 10000`;; val it : thm = |- 0 EXP 10000 = 0