2 (* ---------------------------------------------------------------------- *)
4 (* ---------------------------------------------------------------------- *)
6 let neq = `(=):num->num->bool`;;
7 let nlt = `(<):num->num->bool`;;
8 let ngt = `(>):num->num->bool`;;
9 let nle = `(<=):num->num->bool`;;
10 let nge = `(>=):num->num->bool`;;
11 let nm = `( * ):num->num->num`;;
12 let np = `(+):num->num->num`;;
14 let even_tm = `EVEN`;;
18 let nmax = new_definition(
19 `nmax (n:num) m = if n <= m then m else n`);;
27 let even_tm = `EVEN`;;
30 let k = dest_small_numeral tm in
32 prove(mk_comb(even_tm,tm),ARITH_TAC)
34 prove(mk_comb(odd_tm,tm),ARITH_TAC);;