--- a/Quotient-Paper/document/root.tex	Thu May 27 18:30:42 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Sat May 29 00:16:39 2010 +0200
@@ -20,9 +20,16 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL) is based on a safe logic kernel, which 
-can only be extended by introducing new definitions and new types. 
-
+Higher-order logic (HOL) is based on a small logic kernel, whose 
+only mechanism for extension is the introduction of definitions 
+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
+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 
+can be performed separately. 
 \end{abstract}
 
 % generated text of all theories