# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1665701725 -3600
# Node ID 3ea6a38c33b516b47f000d3068c58aedc1e20649
# Parent  8907d4b6316dfa3ac3cb60d46acc67bfeab5bd97
small polish

diff -r 8907d4b6316d -r 3ea6a38c33b5 thys3/Paper.thy
--- 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