# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1288246603 -32400
# Node ID bf4b28ebb4125125c61168f2aabedb4cdc5e4467
# Parent  26d594a9b89f38f2099f6da5752a9612afcfcd77
Unanonymize qpaper

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.
 
 *}
 
diff -r 26d594a9b89f -r bf4b28ebb412 Quotient-Paper/document/root.tex
--- 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