--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Sat Aug 09 21:03:42 2014 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Sun Aug 10 14:31:06 2014 +0200
@@ -76,12 +76,12 @@
\else
If you want to apply what you have learned about Isabelle we recommend you
donwload and read the book
-\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete
+\href{http://www.concrete-semantics.org}{Concrete
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
programming langage semantics formalised in Isabelle. In fact,
\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
-\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}. The web
-pages for \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}
+\href{http://www.concrete-semantics.org}{Concrete Semantics}. The web
+pages for \href{http://www.concrete-semantics.org}{Concrete Semantics}
also provide a set of \LaTeX-based slides and Isabelle demo files
for teaching \emph{Programming and Proving in Isabelle/HOL}.
\fi