--- a/thys3/Paper.thy	Sun Jul 17 20:09:38 2022 +0100
+++ b/thys3/Paper.thy	Sun Jul 17 20:28:04 2022 +0100
@@ -276,9 +276,9 @@
   \cite{CountingSet2020}). Therefore regular expression matching
   libraries that rely on the classic notion of DFAs often impose 
   adhoc limits for bounded regular expressions: For example in the
-  regular expression matching library in the Go language the regular expression
+  regular expression matching library in the Go language and also in Google's RE2 library the regular expression
   @{term "NTIMES a 1001"} is not permitted, because no counter can be
-  above 1000, and in the built-in Rust regular expression library
+  above 1000; and in the built-in regular expression library in Rust
   expressions such as @{text "a\<^bsup>{1000}{100}{5}\<^esup>"} give an error
   message for being too big.  These problems can of course be solved in matching
   algorithms where automata go beyond the classic notion and for