src/HOL/IntDiv.thy
changeset 29700 22faf21db3df
parent 29668 33ba3faeaa0e
child 29936 d3dfb67f0f59
     1.1 --- a/src/HOL/IntDiv.thy	Fri Jan 30 13:41:45 2009 +0000
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Jan 31 09:04:16 2009 +0100
     1.3 @@ -1173,16 +1173,16 @@
     1.4  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
     1.5    by (rule dvd_trans)
     1.6  
     1.7 -lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
     1.8 +lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
     1.9    by (rule dvd_minus_iff)
    1.10  
    1.11 -lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.12 +lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.13    by (rule minus_dvd_iff)
    1.14  
    1.15 -lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
    1.16 +lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
    1.17    by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
    1.18  
    1.19 -lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    1.20 +lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    1.21    by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
    1.22  
    1.23  lemma zdvd_anti_sym: