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