23 Higher-order logic (HOL) is based on a small logic kernel, whose 

    23 Higher-order logic (HOL) is based on a small logic kernel, whose 

    24 only mechanism for extension is the introduction of definitions 

    24 only mechanism for extension is the introduction of definitions 

    25 and types. Both extensions are often performed by 

    25 and types. Both extensions are often performed by 

    26 quotient constructions, for example finite sets are constructed by quotienting

    26 quotient constructions, for example finite sets are constructed by quotienting

    27 lists, or integers by quotienting pairs of natural numbers. To ease the work 

    27 lists, or integers by quotienting pairs of natural numbers. To ease the work 

    29 the quotient package by Homeier. In doing so we extended his work 

    29 the quotient package by Homeier. In doing so we extended his work 

    30 in order to deal with compositions of quotients. Also, we designed

    30 in order to deal with compositions of quotients. Also, we designed

    31 our quotient package so that every step in a quotient construction 

    31 our quotient package so that every step in a quotient construction 

    32 can be performed separately. 

    32 can be performed separately. 

    33 \end{abstract}

    33 \end{abstract}