--- 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.