--- a/src/HOL/String.thy Sat Nov 11 22:17:14 2023 +0100
+++ b/src/HOL/String.thy Sat Nov 11 17:44:03 2023 +0000
@@ -51,7 +51,7 @@
by (cases c) (simp only: of_char_Char nat_horner_sum)
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
begin
definition char_of :: \<open>'a \<Rightarrow> char\<close>
@@ -439,7 +439,7 @@
end
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
begin
context