--- a/thys3/Paper.thy	Sun Aug 14 09:44:27 2022 +0100
+++ b/thys3/Paper.thy	Mon Aug 15 17:26:08 2022 +0200
@@ -672,7 +672,8 @@
   constants @{text Z} and @{text S}.  The idea with bitcoded regular
   expressions is to incrementally generate the value information (for
   example @{text Left} and @{text Right}) as bitsequences. For this 
-  Sulzmann and Lu define a coding
+  Sulzmann and Lu follow Nielsen and Henglein \cite{NielsenHenglein2011}
+  and define a coding
   function for how values can be coded into bitsequences.
 
   \begin{center}
@@ -708,7 +709,7 @@
   consumed and returns the corresponding value as @{term "Some v"}; otherwise
   it fails with @{text "None"}. We can establish that for a value $v$
   inhabited by a regular expression $r$, the decoding of its
-  bitsequence never fails.
+  bitsequence never fails (see also \cite{NielsenHenglein2011}).
 
   %The decoding can be
   %defined by using two functions called $\textit{decode}'$ and