Mechanizing Set Theory Using Isabelle

L. C. Paulson.
Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389.
L. C. Paulson.
A fixedpoint approach to implementing (co)inductive definitions (revised version). In: A. Bundy (editor), 12th International Conf. on Automated Deduction (Springer LNAI 814, 1994), 148–161.
Slides available
L. C. Paulson.
Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
L. C. Paulson.
Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. (With Krzysztof Grabczewski.)
Slides available
L. C. Paulson.
Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
L. C. Paulson.
The reflection theorem: a study in meta-theoretic reasoning.
In: A. Voronkov (editor), 18th International Conf. on Automated Deduction: CADE-18 (Springer LNAI 2392, 2002), 377–391.
Slides available
L. C. Paulson.
The relative consistency of the axiom of choice — mechanized using Isabelle/ZF.
LMS J. Computation and Mathematics 6 (2003), 198–248.
Slides and theory document available