src/HOL/Presburger.thy
changeset 14353 79f9fbef9106
parent 14271 8ed6989228bb
child 14378 69c4d5997669
     1.1 --- a/src/HOL/Presburger.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -883,7 +883,7 @@
     1.4  next
     1.5    assume ?Q
     1.6    hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
     1.7 -  with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
     1.8 +  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
     1.9    thus ?P by(simp)
    1.10  qed
    1.11