diff -r d1ab5d2d6926 -r 8ddf1330f2ed Quotient-Paper/document/root.tex --- 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.