src/HOL/Library/Code_Abstract_Char.thy

--- a/src/HOL/Library/Code_Abstract_Char.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Abstract_Char.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -18,7 +18,7 @@
 
 lemma char_of_integer_code [code]:
   \<open>integer_of_char (char_of_integer k) = (if 0 \<le> k \<and> k < 256 then k else k mod 256)\<close>
-  by (simp add: integer_of_char_def char_of_integer_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+  by (simp add: integer_of_char_def char_of_integer_def integer_eq_iff integer_less_eq_iff integer_less_iff)
 
 lemma of_char_code [code]:
   \<open>of_char c = of_nat (nat_of_integer (integer_of_char c))\<close>
@@ -104,7 +104,7 @@
   then have \<open>(0 :: integer) \<le> of_char c\<close>
     by (simp only: of_nat_0 of_nat_of_char)
   ultimately show ?thesis
-    by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+    by (simp add: Let_def integer_of_char_def take_bit_eq_mod integer_eq_iff integer_less_eq_iff integer_less_iff)
 next
   case False
   then have \<open>(128 :: integer) \<le> of_char c\<close>
@@ -117,7 +117,7 @@
   then have \<open>of_char c = k + 128\<close>
     by simp
   ultimately show ?thesis
-    by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+    by (simp add: Let_def integer_of_char_def take_bit_eq_mod integer_eq_iff integer_less_eq_iff integer_less_iff)
 qed    
 
 lemma equal_char_code [code]: