64 mechanism for extension is the introduction of safe definitions and of

    64 mechanism for extension is the introduction of safe definitions and of

    65 non-empty types. Both extensions are often performed in quotient

    65 non-empty types. Both extensions are often performed in quotient

    66 constructions. To ease the work involved with such quotient constructions, we

    66 constructions. To ease the work involved with such quotient constructions, we

    67 re-implemented in the popular Isabelle/HOL theorem prover the quotient 

    67 re-implemented in the popular Isabelle/HOL theorem prover the quotient 

    68 package by Homeier. In doing so we extended his work in order to deal with 

    68 package by Homeier. In doing so we extended his work in order to deal with 

    70 of lifting theorems from the raw level to the quotient level.

    70 of lifting theorems from the raw level to the quotient level.

    71 The importance for theorem proving is that many formal

    71 The importance for theorem proving is that many formal

    72 verifications, in order to be feasible, require a convenient resoning infrastructure 

    72 verifications, in order to be feasible, require a convenient resoning infrastructure 

    73 for quotient constructions.

    73 for quotient constructions.

    74 \end{abstract}

    74 \end{abstract}