Abstract
This document contains a proof of the recursion theorem. This is a
mechanization of the proof of the recursion theorem from the text Introduction to
Set Theory, by Karel Hrbacek and Thomas Jech. This
implementation may be used as the basis for a model of Peano arithmetic in
ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development
is much easier to follow.