diff -r 6746f5e1f1f8 -r 12772d537b71 thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Fri Aug 18 14:51:29 2017 +0100
+++ b/thys/Journal/document/root.tex	Fri Aug 25 15:05:20 2017 +0200
@@ -70,7 +70,10 @@
 expressions. They can be used for a very simple regular expression
 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm
 in order to deal with POSIX matching, which is the underlying
-disambiguation strategy for regular expressions needed in lexers.  In
+disambiguation strategy for regular expressions needed in lexers.
+Their algorithm generates POSIX values which encode the information of
+\emph{how} a regular expression matched a string---that is which part
+of the string is matched by which part of the regular expression.  In
 the first part of this paper we give our inductive definition of what
 a POSIX value is and show $(i)$ that such a value is unique (for given
 regular expression and string being matched) and $(ii)$ that Sulzmann