Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF? Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF? If you took your average mathematician on the street and tried to pin down the axiomatics they are implicitly using they'd probably say ZF(C). Even if they couldn't give formal statements of the axioms, that's what they trust could give formal statement of their proofs/results. Why then does a formalization project like Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF in formalizing proofs in things like Analysis? Is there a reason to believe the axiomatization of Isabelle/HOL is stronger/weaker/the same as ZF(C) or is it just incomparable? Are there any relative consistency proofs? Basically, if you believe ZF, why should you believe Isabelle/HOL?
 A: Most people who use Isabelle, use it with HOL. It seems pretty clear that this archive is created by and meant to serve the needs of Isabelle users, so it makes sense the entries will be in the most common theory used with Isabelle. As far as I can tell, this archive does not mandate that you use Isabelle/HOL, and seemingly you could provide an Isabelle/ZF derivation if you wanted.
A quick Google for "isabelle hol set theory" produces this paper, A Formalized Set-Theoretical Semantics for Isabelle/HOL by Rabe and Iancu, which provides a (machine-checked in Twelf) formalization of a ZFC semantics for Isabelle/HOL. I'm confident this is not the first work comparing HOL and ZFC. You can also no doubt find papers with a more precise comparison between HOL and ZFC. Classical HOL is typically treated as having a fairly naive set theoretic semantics.
In practice, I strongly suspect going from informal mathematics to a machine-checked system is, for most math, comparably (and significantly) difficult regardless of the foundation used of the target system if its classical, and often even when it's constructive. Classical versus Constructive is definitely a bigger divide than Set Theory versus Type Theory. Another way of saying this is a good chunk of math is not in any particular foundations, or you could make about as strong a claim that some piece of informal mathematics is "in HOL" as it is "in ZFC".
While I imagine most mathematicians, especially those who can't recite the ZFC axioms, are happy enough to simply assume some suitable metatheoretical work has been done for HOL, this might not be a terrible opportunity to evaluate a foundations directly on its own merit...
