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