src/HOL/Bit_Operations.thy

--- a/src/HOL/Bit_Operations.thy	Thu Nov 09 15:11:51 2023 +0000
+++ b/src/HOL/Bit_Operations.thy	Thu Nov 09 15:11:52 2023 +0000
@@ -2626,7 +2626,7 @@
 subsection \<open>Common algebraic structure\<close>
 
 class unique_euclidean_semiring_with_bit_operations =
-  unique_euclidean_semiring_with_nat + semiring_bit_operations
+  linordered_euclidean_semiring + semiring_bit_operations
 begin
 
 lemma possible_bit [simp]: