src/HOL/Code_Numeral.thy
changeset 67905 fe0f4eeceeb7
parent 67399 eab6ce8368fa
child 68010 3f223b9a0066
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Mar 19 19:24:45 2018 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Mar 20 09:27:39 2018 +0000
     1.3 @@ -889,6 +889,9 @@
     1.4    "division_segment (n::natural) = 1"
     1.5    by (simp add: natural_eq_iff)
     1.6  
     1.7 +instance natural :: linordered_semidom
     1.8 +  by (standard; transfer) simp_all
     1.9 +
    1.10  instance natural :: semiring_parity
    1.11    by (standard; transfer) simp_all
    1.12