--- a/doc-src/Tutorial/basics.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Tutorial/basics.tex Wed Jan 20 18:07:34 1999 +0100
@@ -42,8 +42,12 @@
Everything defined in the parent theories (and their parents \dots) is
automatically visible. To avoid name clashes, identifiers can be qualified by
theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
-available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is
-recommended browsing.
+available online at
+\begin{ttbox}
+http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/
+http://isabelle.in.tum.de/library/HOL/
+\end{ttbox}
+and is recommended browsing.
\begin{warn}
HOL contains a theory \ttindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online