document preparation overview;
Fri, 04 Jan 2002 19:23:28 +0100
changeset 12630 6f2951938b66
parent 12629 281aa36829d8
child 12631 7648ac4a6b95
document preparation overview;
--- 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.
 \hfootref{}{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{}{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
 ML of New Jersey}.