# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1647947642 0
# Node ID d9b672c4c0ac53cffa474fb65a81c9cd116609f5
# Parent  c4b6906068a9ab5ef5205e0388f5881e9a17d9aa
updated

diff -r c4b6906068a9 -r d9b672c4c0ac thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Tue Mar 22 11:08:43 2022 +0000
+++ b/thys2/Paper/Paper.thy	Tue Mar 22 11:14:02 2022 +0000
@@ -1413,7 +1413,9 @@
    see the correct result but find that simplification does not simplify in well-chosen, but not
    obscure, examples. We found that from an implementation
    point-of-view it is really important to have the formal proofs of
-   the corresponding properties at hand. We have also developed a
+   the corresponding properties at hand.
+
+   We have also developed a
    healthy suspicion when experimental data is used to back up
    efficiency claims. For example Sulzmann and Lu write about their
    equivalent of @{term blexer_simp} ``...we can incrementally compute
@@ -1424,7 +1426,7 @@
    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
    tokens according to POSIX rules~\cite{verbatim}. For this it uses Brzozowski's
-   derivatives. 
+   derivatives like in our work. 
    They write: ``The results of our empirical tests [..] confirm that Verbatim has
    @{text "O(n\<^sup>2)"} time complexity.'' \cite[Section~VII]{verbatim}.
    While their correctness proof for Verbatim is formalised in Coq, the claim about
diff -r c4b6906068a9 -r d9b672c4c0ac thys2/paper.pdf
Binary file thys2/paper.pdf has changed