diff -r 59bad592a009 -r 80218dddbb15 thys/Paper/document/root.tex
--- a/thys/Paper/document/root.tex	Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/Paper/document/root.tex	Thu Feb 25 12:17:31 2016 +0000
@@ -15,7 +15,6 @@
 
 \titlerunning{BLA BLA}
 
-
 \urlstyle{rm}
 \isabellestyle{it}
 \renewcommand{\isastyleminor}{\it}%
@@ -28,16 +27,21 @@
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 
 \definecolor{mygrey}{rgb}{.80,.80,.80}
+\def\Brz{Brzozowski}
+
 
 \begin{document}
 
-\title{RegEx}
+\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
 \institute{King's College London, United Kingdom \and 
            St Andrews}
 \maketitle
 
 \begin{abstract}
+\Brz{} introduced the notion of derivatives of regular expressions
+that can be used for very simple regular expression matching algorithms.
+
 BLA BLA  Sulzmann and Lu \cite{Sulzmann2014}
 
 {\bf Keywords:}