diff -r 37d14cbce020 -r 726f4e65c0fe thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Tue Mar 29 10:57:02 2022 +0100
+++ b/thys2/Paper/document/root.tex	Wed Mar 30 18:02:40 2022 +0100
@@ -85,7 +85,7 @@
   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 finite. Without simplification the size of some derivatives can grow
+  derivatives finitely bounded. 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
   variant is a recursive functional program, whereas Sulzmann