--- a/src/Doc/Prog_Prove/Basics.thy Mon Feb 12 13:27:30 2018 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Mon Feb 12 14:13:54 2018 +0100
@@ -126,7 +126,7 @@
In addition to the theories that come with the Isabelle/HOL distribution
(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
there is also the \emph{Archive of Formal Proofs}
-at \<^url>\<open>http://afp.sourceforge.net\<close>, a growing collection of Isabelle theories
+at \<^url>\<open>https://isa-afp.org\<close>, a growing collection of Isabelle theories
that everybody can contribute to.
\subsection{Quotation Marks}
--- a/src/Doc/System/Sessions.thy Mon Feb 12 13:27:30 2018 +0100
+++ b/src/Doc/System/Sessions.thy Mon Feb 12 14:13:54 2018 +0100
@@ -154,7 +154,7 @@
although it uses relatively complex quasi-hierarchic naming conventions like
\<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
names that are relatively long and descriptive, as in the Archive of Formal
- Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
+ Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example.
\<close>
--- a/src/Doc/Tutorial/document/basics.tex Mon Feb 12 13:27:30 2018 +0100
+++ b/src/Doc/Tutorial/document/basics.tex Mon Feb 12 14:13:54 2018 +0100
@@ -95,7 +95,7 @@
For the more adventurous, there is the \emph{Archive of Formal Proofs},
a journal-like collection of more advanced Isabelle theories:
\begin{center}\small
- \url{http://afp.sourceforge.net/}
+ \url{https://isa-afp.org/}
\end{center}
We hope that you will contribute to it yourself one day.%
\index{theories|)}
--- a/src/Doc/manual.bib Mon Feb 12 13:27:30 2018 +0100
+++ b/src/Doc/manual.bib Mon Feb 12 14:13:54 2018 +0100
@@ -1114,7 +1114,7 @@
author = "Andreas Lochbihler",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
- publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+ publisher = "\url{https://isa-afp.org/entries/Coinductive.shtml}",
month = "Feb.",
year = 2010}
@@ -1849,7 +1849,7 @@
author = "Christian Sternagel and Ren\'e Thiemann",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
- publisher = "\url{http://afp.sourceforge.net/entries/Deriving.shtml}",
+ publisher = "\url{https://isa-afp.org/entries/Deriving.shtml}",
month = "March",
year = 2015}