--- a/thys3/Paper.thy	Sat Apr 30 00:55:30 2022 +0100
+++ b/thys3/Paper.thy	Sun May 01 11:50:46 2022 +0100
@@ -1266,7 +1266,7 @@
      
      \noindent
      This means that if the algorithm is called with a regular expression @{term r} and a string
-     @{term s} with $@{term s} \in L(@{term r})$, it will return @{term "Some v"} for the
+     @{term s} with $@{term s} \in L(@{term r})$, it will return @{term "Some v"} for the unique
      @{term v} we defined by the POSIX relation $(@{term s}, @{term r}) \rightarrow @{term v}$; otherwise
      the algorithm returns @{term "None"} when $s \not\in L(r)$ and no such @{text v} exists.
      This completes the correctness proof for the second POSIX lexing algorithm by Sulzmann and Lu.