--- a/AFP-Submission/document/root.tex Tue Jun 14 12:37:46 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-
-\begin{document}
-
-\title{POSIX Lexing with Derivatives of Regular Expressions}
-\author{Fahad Ausaf \and Roy Dyckhoff \and Christian Urban}
-\maketitle
-
-\begin{abstract}
- Brzozowski introduced the notion of derivatives for regular
- expressions. They can be used for a very simple regular expression
- matching algorithm. Sulzmann and Lu \cite{Sulzmann2014} cleverly extended this algorithm
- in order to deal with POSIX matching, which is the underlying
- disambiguation strategy for regular expressions needed in
- lexers. In this entry we give our inductive definition
- of what a POSIX value is and show (i) that such a value is unique (for
- given regular expression and string being matched) and (ii) that
- Sulzmann and Lu's algorithm always generates such a value (provided
- that the regular expression matches the string). We also prove the
- correctness of an optimised version of the POSIX matching
- algorithm.
-\end{abstract}
-
-\tableofcontents
-
-% include generated text of all theories
-\input{session}
-
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}