diff -r 6031383c736a -r 140241dc55e6 doc-src/TutorialI/preface.tex --- 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