Interactive Theorem Proving - Eekelen, Marko; Geuvers, Herman; Kanade, Takeo; Schmaltz, Julien; Wiedijk, Freek (Springer Berlin Heidelberg, 2011)