diff -r 5820841f21fd -r 8cf9d9a3a327 doc-src/TutorialI/preface.tex --- a/doc-src/TutorialI/preface.tex Thu Dec 20 15:17:48 2001 +0100 +++ b/doc-src/TutorialI/preface.tex Thu Dec 20 15:20:07 2001 +0100 @@ -48,16 +48,16 @@ derived almost entirely from output generated in this way. Isabelle's -\href{http://isabelle.in.tum.de/}{web site} +\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, -\href{http://www.proofgeneral.org/}{Proof General}. This book says +\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 \href{http://www.polyml.org/}{Poly/ML}, which is free and +recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best performance. The other supported compiler is -\href{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard +\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