diff -r 79cebcc230d6 -r 231a20534950 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jun 06 13:16:27 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 07 11:33:00 2010 +0200
@@ -46,7 +46,7 @@
    \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}
+    Larry Paulson \cite{Paulson06}
   \end{flushright}\smallskip
 
   \noindent
@@ -58,7 +58,8 @@
   mechanisms for extending the logic: one is the definition of new constants
   in terms of existing ones; the other is the introduction of new types
   by identifying non-empty subsets in existing types. It is well understood 
-  to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
+  to use both mechanisms for dealing with quotient constructions in HOL (see for example 
+  \cite{Paulson06}).
   For example the integers in Isabelle/HOL are constructed by a quotient construction over 
   the type @{typ "nat \<times> nat"} and the equivalence relation