--- a/Quotient-Paper/document/root.tex Sun Jun 13 20:54:50 2010 +0200
+++ b/Quotient-Paper/document/root.tex Mon Jun 14 04:38:25 2010 +0200
@@ -41,7 +41,7 @@
non-empty types. Both extensions are often performed in quotient
constructions. To ease the work involved with such 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
+extended his work in order to deal with compositions of quotients. We also
designed our quotient package so that every step in a quotient construction
can be performed separately and as a result we are able to specify completely
the procedure of lifting theorems from the raw level to the quotient level.