diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Thu Jan 25 15:31:31 2001 +0100
@@ -62,7 +62,7 @@
 
 HOL's theory collection is available online at
 \begin{center}\small
-    \url{http://isabelle.in.tum.de/library/}
+    \url{http://isabelle.in.tum.de/library/HOL/}
 \end{center}
 and is recommended browsing. Note that most of the theories 
 are based on classical Isabelle without the Isar extension. This means that
@@ -233,7 +233,7 @@
 \end{itemize}
 
 For the sake of readability the usual mathematical symbols are used throughout
-the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
+the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
 the appendix.
 
 
@@ -279,7 +279,7 @@
 
 Some interfaces (including the shell level) offer special fonts with
 mathematical symbols. For those that do not, remember that ASCII-equivalents
-are shown in figure~\ref{fig:ascii} in the appendix.
+are shown in table~\ref{tab:ascii} in the appendix.
 
 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
 Commands may but need not be terminated by semicolons.