You can find our Isabelle/HOL formalizations here.
To view them you need to install Isabelle 2017 and the Archive of Formal Proofs (in the Isabelle 2017 version).
We recommend to first run
isabelle build -b -d . PTA_library
and to then start Isabelle with:
isabelle jedit -d . -l PTA_library