diff -r e85d10b238d0 -r 2835d13be702 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Wed May 11 13:12:30 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 16 12:50:37 2016 +0100
@@ -200,7 +200,8 @@
 \noindent {\bf Contributions:} We have implemented in Isabelle/HOL the
 derivative-based regular expression matching algorithm of
 Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this
-algorithm according to our specification of what a POSIX value is. Sulzmann
+algorithm according to our specification of what a POSIX value is (inspired
+by work of Vansummeren \cite{Vansummeren2006}). Sulzmann
 and Lu sketch in \cite{Sulzmann2014} an informal correctness proof: but to
 us it contains unfillable gaps.\footnote{An extended version of
 \cite{Sulzmann2014} is available at the website of its first author; this
@@ -242,7 +243,7 @@
   not match any string, @{const ONE} for the regular expression that matches
   only the empty string and @{term c} for matching a character literal. The
   language of a regular expression is also defined as usual by the
-  recursive function @{term L} with the clauses:
+  recursive function @{term L} with the six clauses:
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{3mm}}rcl}
@@ -492,7 +493,7 @@
   \noindent Note that this function needs only to be partially defined,
   namely only for regular expressions that are nullable. In case @{const
   nullable} fails, the string @{term "[a,b,c]"} cannot be matched by @{term
-  "r\<^sub>1"} and an error is raised instead. Note also how this function
+  "r\<^sub>1"} and the null value @{term "None"} is returned. Note also how this function
   makes some subtle choices leading to a POSIX value: for example if an
   alternative regular expression, say @{term "ALT r\<^sub>1 r\<^sub>2"}, can
   match the empty string and furthermore @{term "r\<^sub>1"} can match the
@@ -774,7 +775,7 @@
   \noindent
   With Lem.~\ref{Posix2} in place, it is completely routine to establish
   that the Sulzmann and Lu lexer satisfies our specification (returning
-  an ``error'' iff the string is not in the language of the regular expression,
+  the null value @{term "None"} iff the string is not in the language of the regular expression,
   and returning a unique POSIX value iff the string \emph{is} in the language):
 
   \begin{theorem}\mbox{}\smallskip\\