src/Provers/Arith/combine_numerals.ML
changeset 15965 f422f8283491
parent 15570 8d8c70b41bab
child 16973 b2a894562b8f
     1.1 --- a/src/Provers/Arith/combine_numerals.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/Provers/Arith/combine_numerals.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -19,11 +19,11 @@
     1.4  signature COMBINE_NUMERALS_DATA =
     1.5  sig
     1.6    (*abstract syntax*)
     1.7 -  val add: int * int -> int          (*addition (or multiplication) *)
     1.8 +  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
     1.9    val mk_sum: typ -> term list -> term
    1.10    val dest_sum: term -> term list
    1.11 -  val mk_coeff: int * term -> term
    1.12 -  val dest_coeff: term -> int * term
    1.13 +  val mk_coeff: IntInf.int * term -> term
    1.14 +  val dest_coeff: term -> IntInf.int * term
    1.15    (*rules*)
    1.16    val left_distrib: thm
    1.17    (*proof tools*)