S. Agerholm and M. Gordon, “Experiments with ZF Set Theory in HOL and Isabelle”, BRICS, vol. 2, no. 37, Jun. 1995.