src/HOL/Code_Numeral.thy
changeset 78955 74147aa81dbb
parent 78937 5e6b195eee83
child 79008 74a4776f7a22
--- 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