1.1 --- a/doc-src/TutorialI/preface.tex Sat Jan 05 01:20:06 2002 +0100
1.2 +++ b/doc-src/TutorialI/preface.tex Sat Jan 05 01:20:52 2002 +0100
1.3 @@ -49,18 +49,18 @@
1.4 The end of Part~I explains how users may produce their own formal documents in
1.5 the same manner.
1.6
1.7 -Isabelle's
1.8 -\hfootref{http://isabelle.in.tum.de/}{web site}
1.9 -contains links to the download area and to documentation and other
1.10 -information. Most Isabelle sessions are now run from within David
1.11 -Aspinall's wonderful user interface,
1.12 -\hfootref{http://www.proofgeneral.org/}{Proof General}. This book says
1.13 -very little about Proof General, which has its own documentation. In
1.14 -order to run Isabelle, you will need a Standard ML compiler. We
1.15 -recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and
1.16 -gives the best performance. The other fully supported compiler is
1.17 -\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
1.18 -ML of New Jersey}.
1.19 +Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
1.20 +the download area and to documentation and other information. Most Isabelle
1.21 +sessions are now run from within David Aspinall's\index{Aspinall, David}
1.22 +wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
1.23 + General}, even together with the
1.24 +\hfootref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}{X-Symbol} package
1.25 +for XEmacs. This book says very little about Proof General, which has its own
1.26 +documentation. In order to run Isabelle, you will need a Standard ML
1.27 +compiler. We recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is
1.28 +free and gives the best performance. The other fully supported compiler is
1.29 +\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
1.30 + New Jersey}.
1.31
1.32 This tutorial owes a lot to the constant discussions with and the valuable
1.33 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf