Isabelle/HOL A Proof Assistant for Higher-Order Logic - Nipkow, Tobias; Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus (Springer Berlin Heidelberg : Imprint: Springer, 2002)