doc-src/TutorialI/basics.tex

     proofs}} in the above theory template.  A complete grammar of the basic
 constructs is found in the Isabelle/Isar Reference Manual.
 
 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
 they look slightly different than the theories in this tutorial, and that all
 proofs are in separate ML files.

 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
 \item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
 \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.
 
 
 \section{Variables}
 \label{sec:variables}

 Isabelle/Isar is the Emacs-based \bfindex{Proof
   General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
 
 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.
 At the shell level it is advisable to use semicolons to enforce that a command
 is executed immediately; otherwise Isabelle may wait for the next keyword