There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar statements that HOL is weaker than CoC or similar because of the lack of dependent types.
Can someone explain what this means? For example, can someone give an example for X and explain why this is not possible to formalize in a system like HOL?
For completeness I'm adding the specific example that the OP is asking for, turning my comment above and Jason Rute's into an answer.
One thing that make type theories occurring in most PAs strictly logically (consistency-wise) stronger is the availability of universes. I would think that one universe is enough to build a model of HOL (and thus showing that is stronger by Gödels 2nd incompleteness theorem). By the same token, “There exists a model of HOL” can't be proved in HOL. On the other hand, Isabelle/HOL includes a theory (ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength.
That said, the great majority of results in math do not need logical strength greater than few orders on top arithmetic: For instance, McLarty showed that Fermat's Last Theorem can be formalized in something like third order arithmetic (while every HOL system provides you with all the finite orders).
Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. This is the point usually made by K. Buzzard.
EDIT: Some references that were kindly provided by user9716869: the document The HOL System Logic provides HOL semantics (effectively in $V(\omega+\omega)$ without the empty set). Sets in Types, Types in Sets shows that ZFC with n inaccessibles can be encoded in CiC with a variant of the Axiom of Choice and $n+1$ universes.
Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL."
A simple example of this is formalising finite dimensional Euclidean spaces -- basically, spaces $\mathbb{R}^n$ where $n$ is a natural number.
The dimension $n$ is a natural example of type dependency, and so proving things about them in HOL is subtle enough that John Harrison wrote a whole TPHOLS paper about it, titled (obviously enough) A HOL Theory of Euclidean space.
ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength. Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. $\endgroup$