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

--- a/Journal/document/root.bib	Sun Nov 20 22:53:50 2011 +0000
+++ b/Journal/document/root.bib	Sat Dec 17 13:32:11 2011 +0000
@@ -59,7 +59,7 @@
   title =        {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
   booktitle =    {The Archive of Formal Proofs},
   editor =       {G.~Klein and T.~Nipkow and L.~Paulson},
-  publisher =    {\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}},
+  publisher =    {\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}},
   month =        Aug,
   year =         2011,
   note =         {Formal proof development},