src/Provers/Arith/combine_numerals.ML

 *)
 
 signature COMBINE_NUMERALS_DATA =
 sig
   (*abstract syntax*)
-  val add: int * int -> int          (*addition (or multiplication) *)
+  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
   val mk_sum: typ -> term list -> term
   val dest_sum: term -> term list
-  val mk_coeff: int * term -> term
-  val dest_coeff: term -> int * term
+  val mk_coeff: IntInf.int * term -> term
+  val dest_coeff: term -> IntInf.int * term
   (*rules*)
   val left_distrib: thm
   (*proof tools*)
   val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
   val trans_tac: thm option -> tactic (*applies the initial lemma*)