diff -r ddf255a4ccc3 -r 5e6b195eee83 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 \Common algebraic structure\ 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]: