src/HOL/String.thy

 lemma nat_of_char [simp]:
   \<open>nat (of_char c) = of_char c\<close>
   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>
   where \<open>char_of n = Char (bit n 0) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close>
 

   "String.explode (String.implode cs) = map ascii_of cs"
   by transfer rule
 
 end
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 context
 begin