Experiments with ZF Set Theory in HOL and Isabelle

Sten Agerholm, Michael J. C. Gordon. Experiments with ZF Set Theory in HOL and Isabelle. In E. Thomas Schubert, Phillip J. Windley, Jim Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings. Volume 971 of Lecture Notes in Computer Science, pages 32-45, Springer, 1995.

@inproceedings{AgerholmG95,
  title = {Experiments with ZF Set Theory in HOL and Isabelle},
  author = {Sten Agerholm and Michael J. C. Gordon},
  year = {1995},
  tags = {C++},
  researchr = {https://researchr.org/publication/AgerholmG95},
  cites = {0},
  citedby = {0},
  pages = {32-45},
  booktitle = {Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop,  Aspen Grove, UT, USA, September 11-14, 1995, Proceedings},
  editor = {E. Thomas Schubert and Phillip J. Windley and Jim Alves-Foss},
  volume = {971},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-60275-5},
}