# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1518441234 -3600
# Node ID 3dd0dfe04fcb6a5a44f214b071300a2ee5dee8fb
# Parent  02cf352cbc4c2e89f9faf1941ec640af26877167
corrected some URLs

diff -r 02cf352cbc4c -r 3dd0dfe04fcb src/Doc/Prog_Prove/Basics.thy
--- 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}
diff -r 02cf352cbc4c -r 3dd0dfe04fcb src/Doc/System/Sessions.thy
--- 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>
 
 
diff -r 02cf352cbc4c -r 3dd0dfe04fcb src/Doc/Tutorial/document/basics.tex
--- 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|)}
diff -r 02cf352cbc4c -r 3dd0dfe04fcb src/Doc/manual.bib
--- 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}