| changeset 24286 | 7619080e49f0 |
| parent 24195 | 7d1a16c77f7c |
| child 24391 | b57c48f7e2d4 |
--- a/src/HOL/IntDiv.thy Wed Aug 15 09:02:11 2007 +0200 +++ b/src/HOL/IntDiv.thy Wed Aug 15 12:52:56 2007 +0200 @@ -1082,7 +1082,7 @@ lemma zdvd_0_right [iff]: "(m::int) dvd 0" by (simp add: dvd_def) -lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" +lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)" by (simp add: dvd_def) lemma zdvd_1_left [iff]: "1 dvd (m::int)"