This is the accompanying material for the paper:

• Higher-order Tarski Grothendieck as a Foundation for Formal Proof

by C.Brown, C.Kaliszyk, and K.Pąk submitted to ITP 2019

It contains the isomorphisms between the Isabelle/HOL and Isabelle/Mizar libraries (subdirectory merge) as well as the Isabelle/Mizar foundations (subdirectory mizar) and a small manually translated part of the MML (subdirectory mml) that the merge theories rely on.

The formalizations are compatible with Isabelle 2018 and can be either compiled or work interactively in the HOL-Number_Theory image.

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 itp19.tgz               26-Mar-2019 11:51  177K