Interactive Theorem Proving - Gerwin Klein, Ruben Gamboa; Gamboa, Ruben; Kittler, Josef (Springer International Publishing, 2014)