src/Provers/Arith/cancel_numerals.ML
changeset 24630 351a308ab58d
parent 20114 a1bb4bc68ff3
child 35762 af3ff2ba4c54
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Tue Sep 18 16:08:00 2007 +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: IntInf.int * term -> term
     1.8 -  val dest_coeff: term -> IntInf.int * term
     1.9 -  val find_first_coeff: term -> term list -> IntInf.int * term list
    1.10 +  val mk_coeff: int * term -> term
    1.11 +  val dest_coeff: term -> int * term
    1.12 +  val find_first_coeff: term -> term list -> int * term list
    1.13    (*rules*)
    1.14    val bal_add1: thm
    1.15    val bal_add2: thm