diff -r 1abf8586ee6b -r aad64c63960e Journal/Paper.thy
--- a/Journal/Paper.thy	Sun Nov 20 22:53:50 2011 +0000
+++ b/Journal/Paper.thy	Sat Dec 17 13:32:11 2011 +0000
@@ -499,7 +499,7 @@
   rest being in @{term "A\<star>"}. We omit
   the proofs for these properties, but invite the reader to consult our
   formalisation.\footnote{Available in the Archive of Formal Proofs at 
-  \url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml} 
+  \url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml} 
   \cite{myhillnerodeafp11}.}
 
   The notation in Isabelle/HOL for the quotient of a language @{text A}
@@ -2474,7 +2474,7 @@
   proof from \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the
   formalisation was not the bottleneck.  The code of
   our formalisation can be found in the Archive of Formal Proofs at
-  \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} 
+  \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}} 
   \cite{myhillnerodeafp11}.\medskip
   
   \noindent