diff -r 26d594a9b89f -r bf4b28ebb412 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Thu Oct 28 14:12:30 2010 +0900 +++ b/Quotient-Paper/Paper.thy Thu Oct 28 15:16:43 2010 +0900 @@ -1279,7 +1279,7 @@ \noindent The code of the quotient package and the examples described here are already included in the standard distribution of Isabelle. -% \footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} + \footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} The package is heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning infrastructure for programming language calculi @@ -1331,11 +1331,11 @@ %% \medskip -% \noindent -% {\bf Acknowledgements:} We would like to thank Peter Homeier for the many -% discussions about his HOL4 quotient package and explaining to us -% some of its finer points in the implementation. Without his patient -% help, this work would have been impossible. + \noindent + {\bf Acknowledgements:} We would like to thank Peter Homeier for the many + discussions about his HOL4 quotient package and explaining to us + some of its finer points in the implementation. Without his patient + help, this work would have been impossible. *}