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