--- a/Quotient-Paper/Paper.thy	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 01 15:58:59 2010 +0200
@@ -36,7 +36,11 @@
 section {* Introduction *}
 
 text {* 
-  {\hfill quote by Larry}\bigskip
+   \begin{flushright}
+  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
+    collect all the theorems we shall ever want into one giant list;''}\\
+    Paulson \cite{Paulson06}
+  \end{flushright}\smallskip
 
   \noindent
   Isabelle is a generic theorem prover in which many logics can be implemented. 

--- a/Quotient-Paper/document/root.bib	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/document/root.bib	Tue Jun 01 15:58:59 2010 +0200
@@ -26,7 +26,7 @@
 
 @techreport{PVS:Interpretations,
         Author= {S. Owre and N. Shankar},
-        Title= {Theory Interpretations in PVS},
+        Title= {{T}heory {I}nterpretations in {PVS}},
         Number= {SRI-CSL-01-01},
         Institution= {Computer Science Laboratory, SRI International},
         Address= {Menlo Park, CA},

--- a/Quotient-Paper/document/root.tex	Tue Jun 01 15:48:25 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Tue Jun 01 15:58:59 2010 +0200
@@ -25,7 +25,7 @@
 and types. Both extensions are often performed by 
 quotient constructions, for example finite sets are constructed by quotienting
 lists, or integers by quotienting pairs of natural numbers. To ease the work 
-involved with quotient construction, we re-implemented in Isabelle/HOL
+involved with quotient constructions, we re-implemented in Isabelle/HOL
 the quotient package by Homeier. In doing so we extended his work 
 in order to deal with compositions of quotients. Also, we designed
 our quotient package so that every step in a quotient construction