--- a/doc-src/TutorialI/preface.tex Sat Jan 05 01:20:06 2002 +0100
+++ b/doc-src/TutorialI/preface.tex Sat Jan 05 01:20:52 2002 +0100
@@ -49,18 +49,18 @@
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}
-contains links to the download area and to documentation and other
-information. Most Isabelle sessions are now run from within David
-Aspinall's wonderful user interface,
-\hfootref{http://www.proofgeneral.org/}{Proof General}. This book says
-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 fully supported compiler is
-\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
-ML of New Jersey}.
+Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
+the download area and to documentation and other information. Most Isabelle
+sessions are now run from within David Aspinall's\index{Aspinall, David}
+wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
+ General}, even together with the
+\hfootref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}{X-Symbol} package
+for XEmacs. This book says 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 fully supported compiler is
+\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
+ New Jersey}.
This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf