Agerholm, S., & Gordon, M. (1995). Experiments with ZF Set Theory in HOL and Isabelle. BRICS Report Series, 2(37). https://doi.org/10.7146/brics.v2i37.19940