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

Slawomir Kolodynski
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

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