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