Agerholm, S., and M. Gordon. “Experiments With ZF Set Theory in HOL and Isabelle”. BRICS Report Series, vol. 2, no. 37, June 1995, doi:10.7146/brics.v2i37.19940.