Interactive Theorem Proving - Urban; Zhang, Xingyuan (Springer International Publishing, 2015)