diff -r 281aa36829d8 -r 6f2951938b66 doc-src/TutorialI/preface.tex
--- 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}.