Isabelle / HOL : a proof assistant for higher-order logic / Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel. - Nipkow, Tobias, 1958- (Lecture notes in computer science, 2002)