# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1660577168 -7200
# Node ID e71a6e2aca2dc23f8d8f5c5a7dc27312a037e3c5
# Parent  f47fc48405798e9d6ef654d0345d253f98116197
updated paper and literature

diff -r f47fc4840579 -r e71a6e2aca2d Literature/Henglein-Nielsen-LATA-paper.pdf
Binary file Literature/Henglein-Nielsen-LATA-paper.pdf has changed
diff -r f47fc4840579 -r e71a6e2aca2d thys3/Paper.thy
--- 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
diff -r f47fc4840579 -r e71a6e2aca2d thys3/document/root.bib
--- a/thys3/document/root.bib	Sun Aug 14 09:44:27 2022 +0100
+++ b/thys3/document/root.bib	Mon Aug 15 17:26:08 2022 +0200
@@ -8,6 +8,18 @@
   pages = {46--90}
 }
 
+@InProceedings{NielsenHenglein2011,
+  author    = {L.~Nielsen and F.~Henglein},
+  title     = {{B}it-{C}oded {R}egular {E}xpression {P}arsing},
+  booktitle = {Proc.~of the 5th International Conference on Language
+               and Automata Theory and Applications (LATA)},
+  year      = {2011},
+  pages     = {402--413},
+  series    = {LNCS},
+  volume    = {6638}
+}
+
+
 @InProceedings{BjorklundMartensTimm2015,
   author = {H.~Bj\"{o}rklund and W.~Martens and T.~Timm},
   title = {{E}fficient {I}ncremental {E}valuation of {S}uccinct