src/Provers/Arith/cancel_numerals.ML
changeset 15965 f422f8283491
parent 15570 8d8c70b41bab
child 16973 b2a894562b8f
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -29,9 +29,9 @@
     1.4    val dest_sum: term -> term list
     1.5    val mk_bal: term * term -> term
     1.6    val dest_bal: term -> term * term
     1.7 -  val mk_coeff: int * term -> term
     1.8 -  val dest_coeff: term -> int * term
     1.9 -  val find_first_coeff: term -> term list -> int * term list
    1.10 +  val mk_coeff: IntInf.int * term -> term
    1.11 +  val dest_coeff: term -> IntInf.int * term
    1.12 +  val find_first_coeff: term -> term list -> IntInf.int * term list
    1.13    (*rules*)
    1.14    val bal_add1: thm
    1.15    val bal_add2: thm