src/HOL/Integ/Presburger.thy
changeset 14378 69c4d5997669
parent 14353 79f9fbef9106
child 14485 ea2707645af8
     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -961,7 +961,7 @@
     1.4    apply (case_tac "0 \<le> k")
     1.5    apply rules
     1.6    apply (simp add: linorder_not_le)
     1.7 -  apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
     1.8 +  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
     1.9    apply assumption
    1.10    apply (simp add: mult_ac)
    1.11    done