--- 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.
*}
--- a/Quotient-Paper/document/root.tex Thu Oct 28 14:12:30 2010 +0900
+++ b/Quotient-Paper/document/root.tex Thu Oct 28 15:16:43 2010 +0900
@@ -45,17 +45,17 @@
\crdata{978-1-4503-0113-8/11/03}
\title{Quotients Revisited for Isabelle/HOL}
-%\numberofauthors{2}
-%\author{
-%\alignauthor
-%Cezary Kaliszyk\\
-% \affaddr{University of Tsukuba, Japan}\\
-% \email{kaliszyk@score.cs.tsukuba.ac.jp}
-%\alignauthor
-%Christian Urban\\
-% \affaddr{Technical University of Munich, Germany}\\
-% \email{urbanc@in.tum.de}
-%}
+\numberofauthors{2}
+\author{
+\alignauthor
+Cezary Kaliszyk\\
+ \affaddr{University of Tsukuba, Japan}\\
+ \email{kaliszyk@cs.tsukuba.ac.jp}
+\alignauthor
+Christian Urban\\
+ \affaddr{Technical University of Munich, Germany}\\
+ \email{urbanc@in.tum.de}
+}
\maketitle