# HG changeset patch
# User wenzelm
# Date 939747865 -7200
# Node ID 7a9270282fd31f3f6551b1e73a8b6fc8afb18520
# Parent  e9cd3f3be589b7381880eeb3d4f3ae964b29af2f
a4paper;
tuned;

diff -r e9cd3f3be589 -r 7a9270282fd3 doc-src/IsarRef/intro.tex
--- 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
diff -r e9cd3f3be589 -r 7a9270282fd3 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Tue Oct 12 18:59:45 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Tue Oct 12 19:04:25 1999 +0200
@@ -1,8 +1,8 @@
 
 %% $Id$
 
-\documentclass[12pt,fleqn]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
 
 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
 \author{\emph{Markus Wenzel} \\ TU M\"unchen}