diff -r db9dba720ac7 -r 74147aa81dbb src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Nov 11 22:17:14 2023 +0100 +++ b/src/HOL/Code_Numeral.thy Sat Nov 11 17:44:03 2023 +0000 @@ -357,7 +357,7 @@ end -instance integer :: unique_euclidean_semiring_with_bit_operations .. +instance integer :: linordered_euclidean_semiring_bit_operations .. context includes bit_operations_syntax @@ -1115,7 +1115,7 @@ end -instance natural :: unique_euclidean_semiring_with_bit_operations .. +instance natural :: linordered_euclidean_semiring_bit_operations .. context includes bit_operations_syntax