--- a/src/HOL/Induct/Ordinals.thy	Mon Sep 05 19:23:12 2022 +0200
+++ b/src/HOL/Induct/Ordinals.thy	Mon Sep 05 20:22:13 2022 +0200
@@ -10,7 +10,7 @@
 
 text \<open>
   Some basic definitions of ordinal numbers.  Draws an Agda
-  development (in Martin-L\"of type theory) by Peter Hancock (see
+  development (in Martin-Löf type theory) by Peter Hancock (see
   \<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
 \<close>