src/HOL/Word/Misc_Numeric.thy
changeset 58681 a478a0742a8e
parent 57512 cc97b347b301
child 58740 cb9d84d3e7f2
     1.1 --- a/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
     1.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  lemma emep1:
     1.5    fixes n d :: int
     1.6    shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
     1.7 -  by (auto simp add: pos_zmod_mult_2 add.commute even_equiv_def)
     1.8 +  by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
     1.9  
    1.10  lemma int_mod_ge:
    1.11    "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"