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