summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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