**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

This entry is a new formalisation of ZFC set theory in Isabelle/HOL. It is logically equivalent to Obua's HOLZF; the point is to have the closest possible integration with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes.

There is a type *V* of sets and a function *elts :: V => V
set* mapping a set to its elements. Classes simply have type *V
set*, and a predicate identifies the small classes: those that correspond
to actual sets. Type classes connected with orders and lattices are used to
minimise the amount of new notation for concepts such as the subset relation,
union and intersection. Basic concepts — Cartesian products, disjoint sums,
natural numbers, functions, etc. — are formalised.

More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals and the transitive closure of a set, are also provided. The definition of addition and multiplication for general sets (not just ordinals) follows Kirby.

The theory provides two type classes with the aim of facilitating
developments that combine *V* with other Isabelle/HOL types:
*embeddable*, the class of types that can be injected into *V*
(including *V* itself as well as *V*V*, etc.), and
*small*, the class of types that correspond to some ZF set.