Quotient-Paper/Paper.thy
changeset 2552 bf4b28ebb412
parent 2551 26d594a9b89f
child 2553 ea0cdb7c6455
--- 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.
 
 *}