--- a/AFP-Submission/README	Tue Jun 14 12:37:46 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-Title:
-======
-POSIX Lexing with Derivatives of Regular Expressions
-
-
-Authors:
-========
-Fahad Ausaf <fahad.ausaf at icloud.com>, 2016
-Roy Dyckhoff <roy.dyckhoff at st-andrews.ac.uk>, 2016
-Christian Urban <christian.urban at kcl.ac.uk>, 2016
-
-
-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 cleverly extended this algorithm
-in order to deal with POSIX matching, which is the underlying
-disambiguation strategy for regular expressions needed in
-lexers. Sulzmann and Lu have made available on-line what they call a
-``rigorous proof'' of the correctness of their algorithm w.r.t. their
-specification; regrettably, it appears to us to have unfillable
-gaps. In the first part of this paper 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. Our definitions and proof are much simpler than those by
-Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
-second part we analyse the correctness argument by Sulzmann and Lu and
-explain why the gaps in this argument cannot be filled easily.
-
-
-New Theories:
-=============
-
- Lexer.thy
- Simplifying.thy
-
-The repository can be checked using Isabelle 2016.
-
- isabelle build -c -v -d . Posix-Lexing
-
-
-  
-
-
-
-
-
-