1 \begin{thebibliography}{10}
4 J.~R. Abrial and G.~Laffitte.
5 \newblock Towards the mechanization of the proofs of some classical theorems of
7 \newblock preprint, February 1993.
10 David Basin and Matt Kaufmann.
11 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
12 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
13 Frameworks}, pages 89--119. Cambridge University Press, 1991.
16 Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
18 \newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
19 \newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
22 J.~Camilleri and T.~F. Melham.
23 \newblock Reasoning with inductively defined relations in the {HOL} theorem
25 \newblock Technical Report 265, Computer Laboratory, University of Cambridge,
28 \bibitem{davey&priestley}
29 B.~A. Davey and H.~A. Priestley.
30 \newblock {\em Introduction to Lattices and Order}.
31 \newblock Cambridge University Press, 1990.
35 \newblock {\em Fundamentals of Contemporary Set Theory}.
36 \newblock Springer, 1979.
40 \newblock {\em Elements of Intuitionism}.
41 \newblock Oxford University Press, 1977.
45 \newblock Contraction-free sequent calculi for intuitionistic logic.
46 \newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
50 \newblock {\em Naive Set Theory}.
51 \newblock Van Nostrand, 1960.
55 \newblock {\em Set Theory: An Introduction to Independence Proofs}.
56 \newblock North-Holland, 1980.
60 \newblock Experimenting with {Isabelle} in {ZF} set theory.
61 \newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
64 Christine Paulin-Mohring.
65 \newblock Inductive definitions in the system {Coq}: Rules and properties.
66 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
71 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
72 \newblock Cambridge University Press, 1987.
74 \bibitem{paulson-set-I}
76 \newblock Set theory for verification: {I}. {From} foundations to functions.
77 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
79 \bibitem{paulson-CADE}
81 \newblock A fixedpoint approach to implementing (co)inductive definitions.
82 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
83 International Conference}, LNAI 814, pages 148--161. Springer, 1994.
85 \bibitem{paulson-final}
87 \newblock A concrete final coalgebra theorem for {ZF} set theory.
88 \newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
89 Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
90 pages 120--139. Springer, 1995.
92 \bibitem{paulson-set-II}
94 \newblock Set theory for verification: {II}. {Induction} and recursion.
95 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
97 \bibitem{paulson-generic}
99 \newblock Generic automatic proof tools.
100 \newblock In Robert Veroff, editor, {\em Automated Reasoning and its
101 Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
105 \newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
106 \newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
110 \newblock {\em Axiomatic Set Theory}.
111 \newblock Dover, 1972.
114 A.~N. Whitehead and B.~Russell.
115 \newblock {\em Principia Mathematica}.
116 \newblock Cambridge University Press, 1962.
117 \newblock Paperback edition to *56, abridged from the 2nd edition (1927).
121 \newblock {\em The Formal Semantics of Programming Languages}.
122 \newblock MIT Press, 1993.
124 \end{thebibliography}