src/HOL/Code_Numeral.thy

 lemma [code]:
   "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
   by transfer (simp add: division_segment_int_def)
 
 instance integer :: ring_parity
-  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+  by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
 
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"

 lemma [code]:
   "division_segment (n::natural) = 1"
   by (simp add: natural_eq_iff)
 
 instance natural :: semiring_parity
-  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+  by (standard; transfer) simp_all
 
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .