changeset 67905 | fe0f4eeceeb7 |
parent 67399 | eab6ce8368fa |
child 68010 | 3f223b9a0066 |
--- 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