# HG changeset patch
# User haftmann
# Date 1521538059 0
# Node ID fe0f4eeceeb78177c2369a973e816b7e83fc175c
# Parent  465f43a9f780b757773dd146643b1e524ffa4580
generalized

diff -r 465f43a9f780 -r fe0f4eeceeb7 src/HOL/Code_Numeral.thy
--- 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
 
diff -r 465f43a9f780 -r fe0f4eeceeb7 src/HOL/Parity.thy
--- 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"