--- a/thys/Journal/Paper.thy	Fri Aug 25 23:52:49 2017 +0200
+++ b/thys/Journal/Paper.thy	Fri Aug 25 23:54:10 2017 +0200
@@ -1277,6 +1277,10 @@
   \end{itemize}
 
   \end{proof}
+
+  To sum up, we have shown that minimal elements according to the ordering
+  by Okui and Suzuki are exactly the @{text POSIX}-values we defined inductively
+  in Section ???
 *}