diff -r 1500f96707b0 -r 3cfea5bb5e23 thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Sun Jan 30 23:37:29 2022 +0000
+++ b/thys2/Paper/document/root.tex	Wed Feb 02 14:52:41 2022 +0000
@@ -65,8 +65,8 @@
   string---that is, which part of the string is matched by which part
   of the regular expression.  The purpose of the bitcodes is to generate POSIX values incrementally while
   derivatives are calculated. They also help with designing
-  an `aggressive' simplification function that keeps the size of
-  derivatives small. Without simplification derivatives can grow
+  an ``aggressive'' simplification function that keeps the size of
+  derivatives small. Without simplification the size derivatives can grow
   exponentially resulting in an extremely slow lexing algorithm.  In this
   paper we describe a variant of Sulzmann and Lu's algorithm: Our
   algorithm is a recursive functional program, whereas Sulzmann