# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1503698050 -7200
# Node ID f46ebc84408db709e758ac85d4f7dd4ad9fe2ff0
# Parent  462d893ecb3d795c0c150b8d168e824d7f482ab2
updated

diff -r 462d893ecb3d -r f46ebc84408d thys/Journal/Paper.thy
--- 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 ???
 *}