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