A mechanized translation from higher-order logic to set theory

In: Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP 2010) (Alexander Krauss and Andreas Schopp) PDF