--- a/Quotient-Paper/document/root.tex	Mon Jun 07 11:33:00 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 07 15:13:39 2010 +0200
@@ -24,18 +24,19 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL), used in several theorem provers, is based on a 
-small logic kernel, whose only mechanism for extension is the introduction 
-of safe definitions and non-empty types. Both extensions are often performed by 
+Higher-order logic (HOL), used in several theorem provers, is based on a small
+logic kernel, whose only mechanism for extension is the introduction of safe
+definitions and non-empty 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 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 
-can be performed separately. The importance to programming language research
-is that many properties of programming languages are more convenient to verify
-over $\alpha$-quotient terms, than over raw terms.
+lists, or integers by quotienting pairs of natural numbers. To ease the work
+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 can be performed separately and as a
+result were able to specify completely the procedure of lifting theorems from
+the raw level to the quotient level.  The importance to programming language
+research is that many properties of programming languages are more convenient
+to verify over $\alpha$-quotient terms, than over raw terms.
 \end{abstract}
 
 % generated text of all theories