diff -r 54eea17575e6 -r 69b4eb4b12c6 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Tue Jun 01 15:48:25 2010 +0200 +++ b/Quotient-Paper/document/root.tex Tue Jun 01 15:58:59 2010 +0200 @@ -25,7 +25,7 @@ and 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 construction, we re-implemented in Isabelle/HOL +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