--- a/thys/Journal/document/root.tex	Wed Aug 15 13:48:57 2018 +0100
+++ b/thys/Journal/document/root.tex	Thu Aug 16 01:12:00 2018 +0100
@@ -50,8 +50,8 @@
   The advantage of the definition based on the
   ordering is that it implements more directly the informal rules from the
   POSIX standard.
-  We also
-  extend our results to additional constructors of regular
+  We also prove Sulzmann \& Lu's conjecture that their bitcoded version
+  of the POSIX algorithm is correct. Furthermore we extend our results to additional constructors of regular
   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
 
 
@@ -82,7 +82,7 @@
 definition of a POSIX value is equivalent to an alternative definition
 by Okui and Suzuki which identifies POSIX values as least elements
 according to an ordering of values.  We also prove the correctness of
-an optimised version of the POSIX matching algorithm and extend the
+Sulzmann's bitcoded version of the POSIX matching algorithm and extend the
 results to additional constructors for regular expressions.  \smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,