src/Provers/Arith/cancel_factor.ML
changeset 15965 f422f8283491
parent 15531 08c8dad8e399
child 19250 932a50e2332f
     1.1 --- a/src/Provers/Arith/cancel_factor.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/Provers/Arith/cancel_factor.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    (*rules*)
     1.5    val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
     1.6    val norm_tac: tactic			(*AC0 etc.*)
     1.7 -  val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
     1.8 +  val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
     1.9  end;
    1.10  
    1.11  signature CANCEL_FACTOR =