diff -r 56837303ce61 -r ab6aaf8d7649 thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Fri Apr 01 23:17:40 2022 +0100
+++ b/thys2/Paper/document/root.tex	Fri Apr 01 23:18:00 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