--- a/thys3/Paper.thy	Thu Oct 13 00:19:50 2022 +0100
+++ b/thys3/Paper.thy	Thu Oct 13 23:55:25 2022 +0100
@@ -1555,7 +1555,7 @@
 transfer to our setting where we are interested in the \emph{size} of the
 derivatives. For example it is not true for our derivatives that the
 set of of derivatives $r \backslash s$ for a given $r$ and all strings
-$s$ is finite. This is because for our annotated regular expressions
+$s$ is finite (even when simplified). This is because for our annotated regular expressions
 the bitcode annotation is dependent on the number of iterations that
 are needed for STAR-regular expressions. This is not a problem for us: Since we intend to do lexing
 by calculating (as fast as possible) derivatives, the bound on the size