MK_BINOP : term -> thm * thm -> thm
# let th1 = NUM_REDUCE_CONV `2 * 2` and th2 = NUM_REDUCE_CONV `2 EXP 2`;; val th1 : thm = |- 2 * 2 = 4 val th2 : thm = |- 2 EXP 2 = 4 # MK_BINOP `(+):num->num->num` (th1,th2);; val it : thm = |- 2 * 2 + 2 EXP 2 = 4 + 4