diff -r d5e9bcb384ec -r 8881a09a06fd thys3/document/root.tex
--- a/thys3/document/root.tex	Wed Oct 12 14:08:06 2022 +0100
+++ b/thys3/document/root.tex	Wed Oct 12 15:23:42 2022 +0100
@@ -1,4 +1,5 @@
-\documentclass[runningheads]{lipics-v2021}
+\documentclass[runningheads]{llncs}
+%!\documentclass[runningheads]{lipics-v2021}
 \usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
@@ -10,7 +11,7 @@
 \usetikzlibrary{positioning}
 %\usepackage{pdfsetup}
 \usepackage{stmaryrd}
-%\usepackage{url}
+\usepackage{url}
 %\usepackage{color}
 %\usepackage[safe]{tipa}
 %\usepackage[sc]{mathpazo}
@@ -58,20 +59,24 @@
 \newtheorem{falsehood}{Falsehood}
 \newtheorem{conject}{Conjecture}
 
-\bibliographystyle{plainurl}
+%!\bibliographystyle{plainurl}
+\bibliographystyle{plain}
 
 \title{{POSIX} {L}exing with {B}itcoded {D}erivatives}
 \titlerunning{POSIX Lexing with Bitcoded Derivatives}
-\author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
-\author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
-\authorrunning{C.~Tan and C.~Urban}
-\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
-\category{}
-\ccsdesc[100]{Design and analysis of algorithms}
-\ccsdesc[100]{Formal languages and automata theory}
-\Copyright{\mbox{}}
-\renewcommand{\DOIPrefix}{}
-\nolinenumbers
+\author{Chengsong Tan\inst{1,2} \and Christian Urban\inst{2}}
+\institute{Imperial College London \and King's College London\\
+\email{\{chengsong.tan,christian.urban\}@kcl.ac.uk}}
+%!\author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
+%!\author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
+%!\authorrunning{C.~Tan and C.~Urban}
+%!\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
+%!\category{}
+%!\ccsdesc[100]{Design and analysis of algorithms}
+%!\ccsdesc[100]{Formal languages and automata theory}
+%!\Copyright{\mbox{}}
+%!\renewcommand{\DOIPrefix}{}
+%!\nolinenumbers
 
 
 \begin{document}
@@ -93,9 +98,10 @@
   paper we describe a variant of Sulzmann and Lu's algorithm: Our
   variant is a recursive functional program, whereas Sulzmann
   and Lu's version involves a fixpoint construction. We \textit{(i)}
-  prove in Isabelle/HOL that our algorithm is correct and generates
-  unique POSIX values; we also \textit{(ii)} establish finite
-  bounds for the size of the derivatives.
+  prove in Isabelle/HOL that our variant is correct and generates
+  unique POSIX values (no such proof has been given for the
+  original algorithm by Sulzmann and Lu); we also \textit{(ii)} establish finite
+  bounds for the size of our derivatives.
 
   %The size can be seen as a
   %proxy measure for the efficiency of the lexing algorithm: because of