--- a/doc-src/TutorialI/preface.tex Fri Jan 04 19:21:15 2002 +0100
+++ b/doc-src/TutorialI/preface.tex Fri Jan 04 19:23:28 2002 +0100
@@ -44,8 +44,10 @@
The typesetting relies on Wenzel's theory presentation tools. An
annotated source file is run, typesetting the theory
% and any requested Isabelle responses
-in the form of a \TeX\ source file. This book is
+in the form of a \LaTeX\ source file. This book is
derived almost entirely from output generated in this way.
+The end of Part~I explains how users may produce their own formal documents in
+the same manner.
Isabelle's
\hfootref{http://isabelle.in.tum.de/}{web site}
@@ -56,7 +58,7 @@
very little about Proof General, which has its own documentation. In
order to run Isabelle, you will need a Standard ML compiler. We
recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and
-gives the best performance. The other supported compiler is
+gives the best performance. The other fully supported compiler is
\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
ML of New Jersey}.