--- a/thys/Journal/document/root.tex	Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Journal/document/root.tex	Fri Aug 18 14:51:29 2017 +0100
@@ -41,11 +41,16 @@
 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a
   revised and expanded version of \cite{AusafDyckhoffUrban2016}.
   Compared with that paper we give a second definition for POSIX
-  values introduced by Okui Suzuki \cite{OkuiSuzuki2013} and prove that it is
+  values introduced by Okui Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech}
+  and prove that it is
   equivalent to our original one. This
   second definition is based on an ordering of values and very similar to,
   but not equivalent with, the
-  definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also
+  definition given by Sulzmann and Lu~\cite{Sulzmann2014}.
+  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
   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
 
@@ -75,9 +80,7 @@
 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. The advantage of the definition based on the
-ordering is that it implements more directly the informal rules from the
-POSIX standard.\smallskip
+ordering of values. \smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL