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_factor.ML
changeset 15965 f422f8283491
parent 15531 08c8dad8e399
child 19250 932a50e2332f 
--- a/src/Provers/Arith/cancel_factor.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/cancel_factor.ML	Mon May 16 10:29:15 2005 +0200
@@ -15,7 +15,7 @@
   (*rules*)
   val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
   val norm_tac: tactic			(*AC0 etc.*)
-  val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
+  val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
 end;
 
 signature CANCEL_FACTOR =
isabelle