# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1464099221 -3600
# Node ID f101eac348f827d3a7fedc33b1e0e2197f12914f
# Parent  6bb15b8e63017e8459cba4f5d3313d5ce96f7231
updated AFP link

diff -r 6bb15b8e6301 -r f101eac348f8 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 24 11:36:21 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue May 24 15:13:41 2016 +0100
@@ -1240,8 +1240,8 @@
   Imp-language is formalised in Coq as part of the Software Foundations book
   by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they
   do not generalise easily to more advanced features.
-  Our formalisation is available from
-  \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip
+  Our formalisation is available from the Archive of Formal Proofs \cite{aduAFP16}
+  under \url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}.\medskip
 
   \noindent
   {\bf Acknowledgements:}
diff -r 6bb15b8e6301 -r f101eac348f8 thys/Paper/document/root.bib
--- a/thys/Paper/document/root.bib	Tue May 24 11:36:21 2016 +0100
+++ b/thys/Paper/document/root.bib	Tue May 24 15:13:41 2016 +0100
@@ -1,4 +1,11 @@
-
+@article{aduAFP16,
+  author =   {Fahad Ausaf and Roy Dyckhoff and Christian Urban},
+  title =    {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
+  journal =  {Archive of Formal Proofs},
+  year =     2016,
+  note =     {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},
+  ISSN =     {2150-914x}
+}
 
 
 @TechReport{CrashCourse2014,
diff -r 6bb15b8e6301 -r f101eac348f8 thys/paper.pdf
Binary file thys/paper.pdf has changed