# HG changeset patch # User paulson # Date 1008858007 -3600 # Node ID 8cf9d9a3a327da25e43f45c59776658f4bc47586 # Parent 5820841f21fd503243ab5081c1fd81073431b841 new hfootref macro for Web links 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 diff -r 5820841f21fd -r 8cf9d9a3a327 doc-src/pdfsetup.sty --- a/doc-src/pdfsetup.sty Thu Dec 20 15:17:48 2001 +0100 +++ b/doc-src/pdfsetup.sty Thu Dec 20 15:20:07 2001 +0100 @@ -1,12 +1,13 @@ \message{pdfsetup.sty v0.1 11/7/2001} \@ifundefined{pdfoutput}{\message{No PDF output}% \usepackage{../url}% - \newcommand{\href}[2]{#2\footnote{#1}}}% + \newcommand{\hfootref}[2]{#2\footnote{#1}}}% {\message{Generating PDF output}% \usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}% \usepackage[pdftex,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}% %no a4paper because overall style sets this (not for Springer!) - \gdef\fnote#1{\hyperpage{#1}n} + \newcommand{\hfootref}[2]{\href{#1}{#2}\footnote{#1}}% + \gdef\fnote#1{\hyperpage{#1}n}% \gdef\bold#1{\textbf{\hyperpage{#1}}}} \urlstyle{rm}