src/HOL/IntDiv.thy
changeset 25112 98824cc791c0
parent 24993 92dfacb32053
child 25134 3d4953e88449
     1.1 --- a/src/HOL/IntDiv.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -1339,7 +1339,7 @@
     1.4    apply simp
     1.5    apply (case_tac "0 \<le> k")
     1.6    apply iprover
     1.7 -  apply (simp add: linorder_not_le)
     1.8 +  apply (simp add: neq0_conv linorder_not_le)
     1.9    apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
    1.10    apply assumption
    1.11    apply (simp add: mult_ac)