--- a/doc-src/IsarRef/intro.tex Tue Oct 12 18:59:45 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Tue Oct 12 19:04:25 1999 +0200
@@ -91,14 +91,24 @@
but a good understanding of mathematical proof might cope with Isar even
better.
-Unfortunately, there is no tutorial on Isabelle/Isar available yet. This
-document really is a \emph{reference manual}. Nevertheless, we will give some
-discussions of the general principles underlying Isar in
+This document really is a \emph{reference manual}. Nevertheless, we will give
+some discussions of the general principles underlying Isar in
chapter~\ref{ch:basics}, and provide some clues of how these may be put into
practice. Some more background information on Isar is given in
-\cite{Wenzel:1999:TPHOL}. Furthermore, there are several examples distributed
-with Isabelle (see directory \texttt{HOL/Isar_examples}).
+\cite{Wenzel:1999:TPHOL}. While there is no proper tutorial on Isabelle/Isar
+available yet, there are several examples distributed with Isabelle. See
+\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the
+Isabelle library:
+\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}
+
+Apart from browsable HTML sources, both example sessions also provide actual
+documents.
%%% Local Variables:
%%% mode: latex