Brian Huffman, Ondrej Kuncar: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. CPP 2013: 131-146