This is the accompanying material for the paper:

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.

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory - [   ] itp19.tgz 26-Mar-2019 11:51 177K
Apache/2.2.3 (Red Hat) Server at Port 80