--- a/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:22 2017 +0200
@@ -282,6 +282,9 @@
"uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
by (simp add: integer_eq_iff)
+instance integer :: ring_parity
+ by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
instantiation integer :: unique_euclidean_semiring_numeral
begin
@@ -927,6 +930,9 @@
"uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
by (simp add: fun_eq_iff)
+instance natural :: semiring_parity
+ by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
.