Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/Arith/cancel_numeral_factor.ML
changeset 24630 351a308ab58d
parent 23261 85f27f79232f
child 35762 af3ff2ba4c54 
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Tue Sep 18 11:06:22 2007 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Tue Sep 18 16:08:00 2007 +0200
@@ -22,8 +22,8 @@
   (*abstract syntax*)
   val mk_bal: term * term -> term
   val dest_bal: term -> term * term
-  val mk_coeff: IntInf.int * term -> term
-  val dest_coeff: term -> IntInf.int * term
+  val mk_coeff: int * term -> term
+  val dest_coeff: term -> int * term
   (*rules*)
   val cancel: thm
   val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
isabelle