# HG changeset patch
# User wenzelm
# Date 1662402133 -7200
# Node ID 24c9f56aa03520d808126a6471f1d947006ed35d
# Parent  f1d75869022225143efb2a498562aea7f39db80d
proper umlauts;

diff -r f1d758690222 -r 24c9f56aa035 src/CTT/ex/Elimination.thy
--- 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).
 *)
 
diff -r f1d758690222 -r 24c9f56aa035 src/Doc/Datatypes/Datatypes.thy
--- 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.
diff -r f1d758690222 -r 24c9f56aa035 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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:
 
diff -r f1d758690222 -r 24c9f56aa035 src/Doc/Locales/Examples3.thy
--- 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
diff -r f1d758690222 -r 24c9f56aa035 src/HOL/Analysis/Lindelof_Spaces.thy
--- 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
diff -r f1d758690222 -r 24c9f56aa035 src/HOL/Data_Structures/Brother12_Set.thy
--- 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" 
diff -r f1d758690222 -r 24c9f56aa035 src/HOL/Induct/Ordinals.thy
--- 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>
 
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
diff -r f1d758690222 -r 24c9f56aa035 src/ZF/ex/misc.thy
--- 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>