--- a/thys/Journal/document/root.tex	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Journal/document/root.tex	Fri Aug 11 20:29:01 2017 +0100
@@ -12,6 +12,9 @@
 %%\usepackage{stmaryrd}
 \usepackage{url}
 \usepackage{color}
+\usepackage[safe]{tipa}
+
+
 
 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
 
@@ -26,6 +29,8 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
+\renewcommand{\isasymin}{\ensuremath{\,\in\,}}
+
 
 \def\Brz{Brzozowski}
 \def\der{\backslash}
@@ -36,8 +41,10 @@
 \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 and prove that it is equivalent to the original one. This
-  definition is based on an ordering of values and very similar to the
+  values introduced by Okui Suzuki \cite{OkuiSuzuki2013} 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
   extend our results to additional constructors of regular
   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
@@ -54,7 +61,6 @@
 \maketitle
 
 \begin{abstract}
-
 Brzozowski introduced the notion of derivatives for regular
 expressions. They can be used for a very simple regular expression
 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm
@@ -68,10 +74,10 @@
 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 a POSIX value as least element according to an
+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 POSIX
-longest-leftmost matching semantics.\smallskip
+ordering is that it implements more directly the informal rules from the
+POSIX standard.\smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL