diff -r 484403cf0c9d -r 6e269f557fc5 thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Tue Mar 22 09:40:24 2022 +0000
+++ b/thys2/Paper/Paper.thy	Tue Mar 22 10:29:07 2022 +0000
@@ -1422,18 +1422,19 @@
    derivatives in some cases even after aggressive simplification, this
    is a hard to believe fact. A similar claim about a theoretical runtime
    of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates
-   POSIX matches and is based on
-   derivatives \cite{verbatim}. In this case derivatives are not even simplified.
-   They write: ``For a specific list of lexical rules, Verbatim has quadratic
-   theoretical time complexity with respect to the length of the input string.''
+   tokens according to POSIX rules \cite{verbatim}. For this it uses Brzozowski's
+   derivatives . 
+   They write: ``The results of our empirical tests [..] confirm that Verbatim has
+   $O(n^2)$ time complexity.'' \cite[Section~VII]{verbatim}.
    While their correctness proof for Verbatim is formalised in Coq, the claim about
-   the runtime complexity is only supported by emperical evidence.
-   When we
-   tried out their extracted OCaml code with our example
-   \mbox{@{text "(a + aa)\<^sup>*"}}, it took around 5 minutes to tokenise a
+   the runtime complexity is only supported by some emperical evidence.
+   In the context of our observation with the ``growth problem'' of derivatives,
+   we
+   tried out their extracted OCaml code with the example
+   \mbox{@{text "(a + aa)\<^sup>*"}} as a single lexing rule, and it took for us around 5 minutes to tokenise a
    string of 40 $a$'s and that increased to approximately 19 minutes when the
-   string was 50 $a$'s long. Given that derivatives are not simplified in
-   the work on Verbatim, such numbers are not surprising. 
+   string is 50 $a$'s long. Given that derivatives are not simplified in the Verbatim
+   lexer, such numbers are not surprising. 
    Clearly our result of having finite
    derivatives might sound rather weak in this context but we think such effeciency claims
    really require further scrutiny.\medskip