--- a/Quotient-Paper/document/root.tex	Mon Jun 07 15:13:39 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 07 15:57:03 2010 +0200
@@ -24,7 +24,7 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL), used in several theorem provers, is based on a small
+Higher-order logic (HOL), used in a number of 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