src/HOL/String.thy

--- a/src/HOL/String.thy	Fri Jul 08 22:30:35 2022 +0200
+++ b/src/HOL/String.thy	Sat Jul 09 08:05:53 2022 +0000
@@ -46,6 +46,10 @@
   \<open>of_int (of_char c) = of_char c\<close>
   by (cases c) simp
 
+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
 begin