This appendix to the paper, The relative consistency of the axiom of choice mechanized using Isabelle, was automatically generated by Isabelle/ZF, and presents the full mechanical development.
The PDF file containing the appendix is: