--- a/Quotient-Paper/Paper.thy	Sun Aug 29 13:36:03 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Mon Aug 30 11:02:13 2010 +0900
@@ -123,7 +123,8 @@
   about raw lambda-terms). In contrast, if we reason about
   $\alpha$-equated lambda-terms, that means terms quotient according to
   $\alpha$-equivalence, then the reasoning infrastructure provided, 
-  for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
+  for example, by Nominal Isabelle %\cite{UrbanKaliszyk11}
+  makes the formal 
   proof of the substitution lemma almost trivial. 
 
   The difficulty is that in order to be able to reason about integers, finite
@@ -645,7 +646,7 @@
   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
   the abstraction function
 
-  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ %%%
   \begin{tabular}{l}
   @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
   \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
@@ -847,7 +848,7 @@
 %%% done it, the theorems need to be 'guessed' from the remaining obligations
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+  @{text "Quot R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
   \end{isabelle}
 
   \noindent
@@ -859,7 +860,7 @@
   \end{isabelle}
 
   \noindent
-  under the assumption @{text "Quotient R Abs Rep"}. The point is that if we have
+  under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have
   an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
   then we need to show this preservation property.
@@ -1245,8 +1246,9 @@
 
   \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/}.} The package is
+  included in the standard distribution of Isabelle.
+%  \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
   involving general binders.  To achieve this, it builds types representing
@@ -1297,11 +1299,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	Sun Aug 29 13:36:03 2010 +0800
+++ b/Quotient-Paper/document/root.tex	Mon Aug 30 11:02:13 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@score.cs.tsukuba.ac.jp}
+%\alignauthor
+%Christian Urban\\
+%  \affaddr{Technical University of Munich, Germany}\\
+%  \email{urbanc@in.tum.de}
+%}
 
 \maketitle