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