  A logic for specification and verification is derived from the axioms of
Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant
Isabelle. Isabelle is generic, supporting several different logics. Isabelle
has the flexibility to adapt to variants of set theory. Its higher-order syntax
supports the definition of new binding operators. Unknowns in subgoals can be
instantiated incrementally. The paper describes the derivation of rules for
descriptions, relations and functions, and discusses interactive proofs of
Cantor's Theorem, the Composition of Homomorphisms challenge [9], and Ramsey's
Theorem [5]. A generic proof assistant can stand up against provers dedicated
to particular logics.
