--- 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:}

--- 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,

Binary file thys/paper.pdf has changed