--- 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.
*}