--- a/src/HOL/Code_Numeral.thy Mon Mar 19 19:24:45 2018 +0100
+++ b/src/HOL/Code_Numeral.thy Tue Mar 20 09:27:39 2018 +0000
@@ -889,6 +889,9 @@
"division_segment (n::natural) = 1"
by (simp add: natural_eq_iff)
+instance natural :: linordered_semidom
+ by (standard; transfer) simp_all
+
instance natural :: semiring_parity
by (standard; transfer) simp_all
--- a/src/HOL/Parity.thy Mon Mar 19 19:24:45 2018 +0100
+++ b/src/HOL/Parity.thy Tue Mar 20 09:27:39 2018 +0000
@@ -11,7 +11,7 @@
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
-class semiring_parity = linordered_semidom + unique_euclidean_semiring +
+class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring +
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"