--- a/Quotient-Paper/document/root.tex	Fri Aug 27 19:06:30 2010 +0800
+++ b/Quotient-Paper/document/root.tex	Fri Aug 27 23:26:00 2010 +0800
@@ -66,7 +66,7 @@
 constructions. To ease the work involved with such quotient constructions, we
 re-implemented in the popular Isabelle/HOL theorem prover the quotient 
 package by Homeier. In doing so we extended his work in order to deal with 
-compositions of quotients and we are also able to specify completely the procedure 
+compositions of quotients and also specified completely the procedure 
 of lifting theorems from the raw level to the quotient level.
 The importance for theorem proving is that many formal
 verifications, in order to be feasible, require a convenient resoning infrastructure