Agerholm, S.; Gordon, M. Experiments With ZF Set Theory in HOL and Isabelle. BRICS 1995, 2.