diff -r f1d758690222 -r 24c9f56aa035 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Mon Sep 05 19:23:12 2022 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Mon Sep 05 20:22:13 2022 +0200
@@ -31,7 +31,7 @@
   We represent $\omega$-words as functions from the natural numbers
   to the alphabet type. Other possible formalizations include
   a coinductive definition or a uniform encoding of finite and
-  infinite words, as studied by M\"uller et al.
+  infinite words, as studied by Müller et al.
 \<close>
 
 type_synonym