--- a/doc-src/Tutorial/basics.tex Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/basics.tex Mon May 10 17:43:55 1999 +0200
@@ -42,10 +42,14 @@
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
-\begin{ttbox}
-http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/
-http://isabelle.in.tum.de/library/HOL/
-\end{ttbox}
+
+\begin{center}\small
+ \begin{tabular}{l}
+ \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
+ \url{http://isabelle.in.tum.de/library/} \\
+ \end{tabular}
+\end{center}
+
and is recommended browsing.
\begin{warn}
HOL contains a theory \ttindexbold{Main}, the union of all the basic