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 24993 92dfacb32053
parent 24630 351a308ab58d
child 25112 98824cc791c0 
--- a/src/HOL/IntDiv.thy	Fri Oct 12 08:20:45 2007 +0200
+++ b/src/HOL/IntDiv.thy	Fri Oct 12 08:20:46 2007 +0200
@@ -1144,7 +1144,7 @@
   by (simp add: dvd_def zmod_eq_0_iff)
 
 instance int :: dvd_mod
-  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
+  by default (simp add: zdvd_iff_zmod_eq_0)
 
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
isabelle