--- a/doc-src/TutorialI/preface.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/TutorialI/preface.tex Sat Apr 28 16:06:30 2012 +0200
@@ -35,17 +35,11 @@
from output generated in this way. The final chapter of Part~I explains how
users may produce their own formal documents in a similar fashion.
-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://proofgeneral.inf.ed.ac.uk/}{Proof
- General}, even together with the
-\hfootref{http://x-symbol.sourceforge.net}{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://www.smlnj.org/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.
+The classic Isabelle user interface is Proof~General~/ Emacs by David
+Aspinall's\index{Aspinall, David}. This book says very little about
+Proof General, which has its own documentation.
This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf