# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1519420117 0
# Node ID 12a8dfcb55a7e5f1edf40dd06a0ad51bc17a4d22
# Parent  5191a09d9928dc5558eeef7e35fa0bc28f29124e
updated

diff -r 5191a09d9928 -r 12a8dfcb55a7 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Feb 06 14:38:31 2018 +0000
+++ b/Journal/Paper.thy	Fri Feb 23 21:08:37 2018 +0000
@@ -2383,13 +2383,18 @@
   The code of our formalisation 
   can be downloaded from the Mercurial repository at
   \url{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi/pip}.
-
-  %\medskip
+  \medskip
 
-  %\noindent
-  %{\bf Acknowledgements:}
-  %We are grateful for the comments we received from anonymous
-  %referees.
+  \noindent {\bf Acknowledgements:} We are grateful for the comments
+  we received from anonymous referees. We are also deeply saddened about the
+  tragic death of our co-author, colleague and friend, Chunhan, who
+  suddenly died on 22 December 2016. He drove very much forward this work
+  and extended it in his PhD-thesis with a formal verification of an
+  SELinux-style access control system. He was a stellar student
+  and very promising young researcher in the field of interactive
+  theorem proving. He was liked by many and indispensable for
+  organising the ITP'15 conference in Nanjing. Chunhan left behind a
+  grieving wife and eight-year-old son.
 
   \bibliographystyle{plain}
   \bibliography{root}
diff -r 5191a09d9928 -r 12a8dfcb55a7 journal.pdf
Binary file journal.pdf has changed