Its nice to be able to use the proper mathematical characters in such a development. In the original work this was done using an extension to the Cambridge HOL system, consisting of filters before and after which mapped non-ascii characters on to sequences of ascii characters in HOL.
A similar approach to supporting an extended character set was later used in ProofPower, and I have now replicated the axiomatisation of ZFC in HOL under ProofPower.
The axiomatisation of ZFC in HOL followed closely that presented in Hatcher. This was intended to make the axiomatisation as uncontroversial as possible, and reduce the scope for errors arising the axiomatisation. A neater axiomatisation is most probably achievable but this would have none other that aesthetic advantages over the one adopted.