S. Agerholm og M. Gordon, “Experiments with ZF Set Theory in HOL and Isabelle”, BRICS, bd. 2, nr. 37, jun. 1995.