Re: [isabelle] An ATP question



> it also works with Metamath somehow.  

I translated about 600 proofs from Metamath to Isabelle/ZF. So it was the other way than what Michael asked about. There are some details in http://isarmathlib.org/MMI_prelude.html.

Slawomir Kolodynski


http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.