Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IMP/HoareEx.thy
changeset 72835 66ca5016b008
parent 67443 3abf6a722518
child 76987 4c275405faae 
--- 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>
isabelle