--- 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>
--- 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.
*)
--- 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>
--- 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