diff -r 692b62426677 -r deea42c83c9e thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/Journal/document/root.tex	Thu Oct 05 12:45:13 2017 +0100
@@ -72,7 +72,7 @@
 in order to deal with POSIX matching, which is the underlying
 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
+\emph{how} a regular expression matches a string---that is, which part
 of the string is matched by which part of the regular expression.  In
 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