changeset 47217 | 501b9bbd0d6e |
parent 47167 | 099397de21e3 |
child 47255 | 30a1692557b0 |
--- a/src/HOL/Divides.thy Fri Mar 30 10:41:27 2012 +0200 +++ b/src/HOL/Divides.thy Fri Mar 30 11:16:35 2012 +0200 @@ -1086,7 +1086,7 @@ by (simp add: numeral_2_eq_2 le_mod_geq) lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" -by (simp add: nat_mult_2 [symmetric]) +by (simp add: mult_2 [symmetric]) lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1" proof -