src/HOL/Word/Bit_Representation.thy

 where
   "bin_last w \<longleftrightarrow> w mod 2 = 1"
 
 lemma bin_last_odd:
   "bin_last = odd"
-  by (rule ext) (simp add: bin_last_def even_def)
+  by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero)
 
 definition bin_rest :: "int \<Rightarrow> int"
 where
   "bin_rest w = w div 2"
 

   apply (simp add: bin_last_def bin_rest_def Bit_def)
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
      apply auto
-  apply (auto simp: even_def)
+  apply (auto simp: even_iff_mod_2_eq_zero)
   done
 
 subsection "Simplifications for (s)bintrunc"
 
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"