src/HOL/Library/Omega_Words_Fun.thy
changeset 76063 24c9f56aa035
parent 69597 ff784d5a5bfb
child 76231 8a48e18f081e
--- 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