--- a/thys/Paper/document/root.tex	Thu Feb 25 20:13:41 2016 +0000
+++ b/thys/Paper/document/root.tex	Sun Feb 28 14:01:12 2016 +0000
@@ -39,12 +39,29 @@
 \maketitle
 
 \begin{abstract}
-\Brz{} introduced the notion of derivatives of regular expressions
-that can be used for very simple regular expression matching algorithms.
 
-BLA BLA  Sulzmann and Lu \cite{Sulzmann2014}
+\Brz{} 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
+in order to deal with POSIX matching, which is the underlying
+disambiguation strategy for regular expressions needed in
+lexers. Sulzmann and Lu have made available on-line what they call a
+``rigorous proof'' of the correctness of their algorithm w.r.t.~their
+specification; regrettably, it appears to us to have unfillable gaps.
+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. Our definitions and proof are much simpler than those by
+Sulzmann and Lu and can be easily formalised in Isabelle/HOL.  In the
+second part we analyse the correctness argument by Sulzmann and Lu in
+more detail and explain why it seems hard to turn it into a proof
+rigorous enough to be accepted by a system such as Isabelle/HOL.
 
-{\bf Keywords:} 
+{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
+Isabelle/HOL
 \end{abstract}
 
 \input{session}