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