\begin{thebibliography}{10}
\bibitem{abrial93}
J.~R. Abrial and G.~Laffitte.
\newblock Towards the mechanization of the proofs of some classical theorems of
set theory.
\newblock preprint, February 1993.
\bibitem{basin91}
David Basin and Matt Kaufmann.
\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
Frameworks}, pages 89--119. Cambridge University Press, 1991.
\bibitem{boyer86}
Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
Lawrence Wos.
\newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
\bibitem{camilleri92}
J.~Camilleri and T.~F. Melham.
\newblock Reasoning with inductively defined relations in the {HOL} theorem
prover.
\newblock Technical Report 265, Computer Laboratory, University of Cambridge,
August 1992.
\bibitem{davey&priestley}
B.~A. Davey and H.~A. Priestley.
\newblock {\em Introduction to Lattices and Order}.
\newblock Cambridge University Press, 1990.
\bibitem{devlin79}
Keith~J. Devlin.
\newblock {\em Fundamentals of Contemporary Set Theory}.
\newblock Springer, 1979.
\bibitem{dummett}
Michael Dummett.
\newblock {\em Elements of Intuitionism}.
\newblock Oxford University Press, 1977.
\bibitem{dyckhoff}
Roy Dyckhoff.
\newblock Contraction-free sequent calculi for intuitionistic logic.
\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
\bibitem{halmos60}
Paul~R. Halmos.
\newblock {\em Naive Set Theory}.
\newblock Van Nostrand, 1960.
\bibitem{kunen80}
Kenneth Kunen.
\newblock {\em Set Theory: An Introduction to Independence Proofs}.
\newblock North-Holland, 1980.
\bibitem{noel}
Philippe No{\"e}l.
\newblock Experimenting with {Isabelle} in {ZF} set theory.
\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
\bibitem{paulin92}
Christine Paulin-Mohring.
\newblock Inductive definitions in the system {Coq}: Rules and properties.
\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
December 1992.
\bibitem{paulson87}
Lawrence~C. Paulson.
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
\newblock Cambridge University Press, 1987.
\bibitem{paulson-set-I}
Lawrence~C. Paulson.
\newblock Set theory for verification: {I}. {From} foundations to functions.
\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
\bibitem{paulson-CADE}
Lawrence~C. Paulson.
\newblock A fixedpoint approach to implementing (co)inductive definitions.
\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
International Conference}, LNAI 814, pages 148--161. Springer, 1994.
\bibitem{paulson-final}
Lawrence~C. Paulson.
\newblock A concrete final coalgebra theorem for {ZF} set theory.
\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
pages 120--139. Springer, 1995.
\bibitem{paulson-set-II}
Lawrence~C. Paulson.
\newblock Set theory for verification: {II}. {Induction} and recursion.
\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
\bibitem{paulson-generic}
Lawrence~C. Paulson.
\newblock Generic automatic proof tools.
\newblock In Robert Veroff, editor, {\em Automated Reasoning and its
Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
\bibitem{quaife92}
Art Quaife.
\newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
\bibitem{suppes72}
Patrick Suppes.
\newblock {\em Axiomatic Set Theory}.
\newblock Dover, 1972.
\bibitem{principia}
A.~N. Whitehead and B.~Russell.
\newblock {\em Principia Mathematica}.
\newblock Cambridge University Press, 1962.
\newblock Paperback edition to *56, abridged from the 2nd edition (1927).
\bibitem{winskel93}
Glynn Winskel.
\newblock {\em The Formal Semantics of Programming Languages}.
\newblock MIT Press, 1993.
\end{thebibliography}