# HG changeset patch
# User wenzelm
# Date 1607258965 -3600
# Node ID 66ca5016b008424a3bde2cfa179d7b44366c854b
# Parent  a025f845fd41697f21a6b0f17a25acf354df8f52
more Unicode;

diff -r a025f845fd41 -r 66ca5016b008 src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Dec 06 13:44:07 2020 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Dec 06 13:49:25 2020 +0100
@@ -8,7 +8,7 @@
 theory HoareEx imports Denotational begin
 
 text \<open>
-  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
+  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
   @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 \<close>
diff -r a025f845fd41 -r 66ca5016b008 src/HOL/HOLCF/IOA/ABP/Check.ML
--- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Sun Dec 06 13:44:07 2020 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Sun Dec 06 13:49:25 2020 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/HOLCF/IOA/ABP/Check.ML
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
 
 The Model Checker.
 *)
diff -r a025f845fd41 -r 66ca5016b008 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Sun Dec 06 13:44:07 2020 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Sun Dec 06 13:49:25 2020 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/HOLCF/Lift.thy
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
 *)
 
 section \<open>Lifting types of class type to flat pcpo's\<close>
diff -r a025f845fd41 -r 66ca5016b008 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Dec 06 13:44:07 2020 +0100
+++ b/src/HOL/ROOT	Sun Dec 06 13:49:25 2020 +0100
@@ -1125,7 +1125,7 @@
 
 session IOA (timing) in "HOLCF/IOA" = HOLCF +
   description "
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
     Copyright   1997 TU München
 
     A formalization of I/O automata in HOLCF.
@@ -1138,7 +1138,7 @@
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description "
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
 
     The Alternating Bit Protocol performed in I/O-Automata:
     combining IOA with Model Checking.
@@ -1158,7 +1158,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 
     A network transmission protocol, performed in the
-    I/O automata formalization by Olaf Mueller.
+    I/O automata formalization by Olaf Müller.
   "
   theories
     Overview
@@ -1166,7 +1166,7 @@
 
 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   description "
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
 
     Memory storage case study.
   "
@@ -1174,7 +1174,7 @@
 
 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   description "
-    Author:     Olaf Mueller
+    Author:     Olaf Müller
   "
   theories
     TrivEx