1signature Arith_cons = 2sig 3 include Abbrev 4 type int = Arbint.int 5 6 val num_ty : hol_type 7 val mk_plus : term * term -> term 8 val mk_minus : term * term -> term 9 val mk_mult : term * term -> term 10 val dest_plus : term -> term * term 11 val dest_minus : term -> term * term 12 val dest_mult : term -> term * term 13 val is_plus : term -> bool 14 val is_minus : term -> bool 15 val is_mult : term -> bool 16 val mk_less : term * term -> term 17 val mk_leq : term * term -> term 18 val mk_greater : term * term -> term 19 val mk_geq : term * term -> term 20 val dest_less : term -> term * term 21 val dest_leq : term -> term * term 22 val dest_greater : term -> term * term 23 val dest_geq : term -> term * term 24 val is_less : term -> bool 25 val is_leq : term -> bool 26 val is_greater : term -> bool 27 val is_geq : term -> bool 28 val is_num_reln : term -> bool 29 val mk_suc : term -> term 30 val dest_suc : term -> term 31 val is_suc : term -> bool 32 val mk_pre : term -> term 33 val dest_pre : term -> term 34 val is_pre : term -> bool 35 val is_num_const : term -> bool 36 val is_zero : term -> bool 37 val int_of_term : term -> int 38 val term_of_int : int -> term 39 val mk_num_var : string -> term 40 val arg1 : term -> term 41 val arg2 : term -> term 42end 43