1new_theory `exp`;; 2 3let REV_EXP = new_prim_rec_definition ( 4 `REV_EXP`, 5 "(REV_EXP 0 n = 1) /\ 6 (REV_EXP (SUC m) n = (n * (REV_EXP m n)))");; 7 8let EXP = new_infix_definition ( 9 `EXP`, 10 "$EXP n m = REV_EXP m n");; 11 12let EXP = prove_thm ( 13 `EXP`, 14 "(m EXP 0 = 1) /\ (m EXP (SUC n) = m * (m EXP n))", 15 REWRITE_TAC [EXP;REV_EXP]);; 16 17close_theory ();; 18