# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1651402246 -3600
# Node ID ab626b60ee64c7a0ba3f4fb59d18a7c8afbe2977
# Parent  04b5e904a2206d65ab480c0671a217622f76f9e8
fixed tiny typo in the paper

diff -r 04b5e904a220 -r ab626b60ee64 thys3/Paper.thy
--- 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.