Theorem Proving in Higher Order Logics - Berghofer, Stefan; Kanade, Takeo; Nipkow, Tobias; Urban, Christian; Wenzel, Makarius (Springer Berlin Heidelberg, 2009)