Isabelle/HOL: A proof assistant for higher-order logic Tobias Nipkow, Markus Wenzel, Lawrence C. Paulson [doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] Springer-Verlag Berlin, Heidelberg 2002 Note(s): interactive theorem prover