diff -r fb23e3fd12e5 -r b7199d6c672d thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Feb 08 01:25:26 2022 +0000
+++ b/thys/Paper/Paper.thy	Tue Feb 08 14:29:41 2022 +0000
@@ -431,9 +431,11 @@
   \end{proposition}
 
   In general there is more than one value associated with a regular
-  expression. In case of POSIX matching the problem is to calculate the
-  unique value that satisfies the (informal) POSIX rules from the
-  Introduction. Graphically the POSIX value calculation algorithm by
+  expression (meaining regular expressions can typically match more
+  than one string). But even given a string from the language of the
+  regular expression, there are generally more than one way how the
+  regular expression can match this string. POSIX lexing is about identifying
+  a unique value that satisfies the (informal) POSIX. Graphically the POSIX value calculation algorithm by
   Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz}
   where the path from the left to the right involving @{term derivatives}/@{const
   nullable} is the first phase of the algorithm (calculating successive