--- a/src/CTT/ex/Elimination.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/CTT/ex/Elimination.thy Mon Sep 05 20:22:13 2022 +0200
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Some examples taken from P. Martin-L\"of, Intuitionistic type theory
+Some examples taken from P. Martin-Löf, Intuitionistic type theory
(Bibliopolis, 1984).
*)
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 05 20:22:13 2022 +0200
@@ -3679,7 +3679,7 @@
Lars Noschinski implemented the @{command simps_of_case} and @{command
case_of_simps} commands. Florian Haftmann, Christian Urban, and Makarius
Wenzel provided general advice on Isabelle and package writing. Stefan Milius
-and Lutz Schr\"oder found an elegant proof that eliminated one of the BNF
+and Lutz Schröder found an elegant proof that eliminated one of the BNF
proof obligations. Mamoun Filali-Amine, Gerwin Klein, Andreas Lochbihler,
Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
this tutorial.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Sep 05 20:22:13 2022 +0200
@@ -2076,7 +2076,7 @@
\<close>
-section \<open>Algebraic reasoning via Gr\"obner bases\<close>
+section \<open>Algebraic reasoning via Gröbner bases\<close>
text \<open>
\begin{matharray}{rcl}
@@ -2092,7 +2092,7 @@
@@{attribute (HOL) algebra} (() | 'add' | 'del')
\<close>
- \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases,
+ \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gröbner bases,
see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
The method handles deals with two main classes of problems:
--- a/src/Doc/Locales/Examples3.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/Doc/Locales/Examples3.thy Mon Sep 05 20:22:13 2022 +0200
@@ -506,7 +506,7 @@
mechanisms, which are described in another paper by Haftmann and
Wenzel~@{cite HaftmannWenzel2009}.
- The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}
+ The original work of Kammüller on locales~@{cite KammullerEtAl1999}
may be of interest from a historical perspective. My previous
report on locales and locale expressions~@{cite Ballarin2004a}
describes a simpler form of expressions than available now and is
--- a/src/HOL/Analysis/Lindelof_Spaces.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Mon Sep 05 20:22:13 2022 +0200
@@ -1,4 +1,4 @@
-section\<open>Lindel\"of spaces\<close>
+section\<open>Lindelöf spaces\<close>
theory Lindelof_Spaces
imports T1_Spaces
--- a/src/HOL/Data_Structures/Brother12_Set.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Mon Sep 05 20:22:13 2022 +0200
@@ -488,7 +488,7 @@
subsection \<open>Height-Size Relation\<close>
-text \<open>By Daniel St\"uwe\<close>
+text \<open>By Daniel Stüwe\<close>
fun fib_tree :: "nat \<Rightarrow> unit bro" where
"fib_tree 0 = N0"
--- 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>
--- 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
--- a/src/ZF/ex/misc.thy Mon Sep 05 19:23:12 2022 +0200
+++ b/src/ZF/ex/misc.thy Mon Sep 05 20:22:13 2022 +0200
@@ -71,7 +71,7 @@
text\<open>Given as a challenge problem in
R. Boyer et al.,
- Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
+ Set Theory in First-Order Logic: Clauses for Gödel's Axioms,
JAR 2 (1986), 287-327\<close>
text\<open>collecting the relevant lemmas\<close>