1.1 --- a/doc-src/TutorialI/basics.tex	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  HOL's theory collection is available online at
     1.6  \begin{center}\small
     1.7 -    \url{http://isabelle.in.tum.de/library/}
     1.8 +    \url{http://isabelle.in.tum.de/library/HOL/}
     1.9  \end{center}
    1.10  and is recommended browsing. Note that most of the theories 
    1.11  are based on classical Isabelle without the Isar extension. This means that
    1.12 @@ -233,7 +233,7 @@
    1.13  \end{itemize}
    1.14  
    1.15  For the sake of readability the usual mathematical symbols are used throughout
    1.16 -the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
    1.17 +the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
    1.18  the appendix.
    1.19  
    1.20  
    1.21 @@ -279,7 +279,7 @@
    1.22  
    1.23  Some interfaces (including the shell level) offer special fonts with
    1.24  mathematical symbols. For those that do not, remember that ASCII-equivalents
    1.25 -are shown in figure~\ref{fig:ascii} in the appendix.
    1.26 +are shown in table~\ref{tab:ascii} in the appendix.
    1.27  
    1.28  Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
    1.29  Commands may but need not be terminated by semicolons.