diff -r 12772d537b71 -r 462d893ecb3d thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Fri Aug 25 15:05:20 2017 +0200
+++ b/thys/Journal/document/root.tex	Fri Aug 25 23:52:49 2017 +0200
@@ -72,18 +72,17 @@
 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 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
-and Lu's algorithm always generates such a value (provided that the
-regular expression matches the string). We also prove the correctness
-of an optimised version of the POSIX matching algorithm.  In the
-second part we show that $(iii)$ our inductive 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. \smallskip
+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 and Lu's
+algorithm always generates such a value (provided that the regular
+expression matches the string). We show that $(iii)$ our inductive
+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.  \smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL