This is an unofficial reimagining of the Archive of Formal Proofs
Recursion Theorem in ZFby Georgy Dunaev