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