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/HOL/IntDiv.thy
changeset 25112 98824cc791c0
parent 24993 92dfacb32053
child 25134 3d4953e88449 
--- a/src/HOL/IntDiv.thy	Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/IntDiv.thy	Sat Oct 20 12:09:33 2007 +0200
@@ -1339,7 +1339,7 @@
   apply simp
   apply (case_tac "0 \<le> k")
   apply iprover
-  apply (simp add: linorder_not_le)
+  apply (simp add: neq0_conv linorder_not_le)
   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
   apply (simp add: mult_ac)
isabelle