--- a/thys2/Paper/document/root.tex	Tue Feb 08 14:29:41 2022 +0000
+++ b/thys2/Paper/document/root.tex	Wed Feb 09 00:29:04 2022 +0000
@@ -63,7 +63,7 @@
 \author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
 \author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
 \authorrunning{C.~Tan and C.~Urban}
-\keywords{POSIX matching and lexing, Derivatives of Regular Expressions, Isabelle/HOL}
+\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
 \category{}
 \ccsdesc[100]{Design and analysis of algorithms}
 \ccsdesc[100]{Formal languages and automata theory}
@@ -88,7 +88,7 @@
   derivatives finite. Without simplification the size of some derivatives can grow
   arbitrarily big 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
+  variant is a recursive functional program, whereas Sulzmann
   and Lu's version involves a fixpoint construction. We \textit{(i)}
   prove in Isabelle/HOL that our algorithm is correct and generates
   unique POSIX values; we also \textit{(ii)} establish a finite