Metamath to GHilbert conversion program

[Steven]

I've read mentions of a program that can convert .mm files into
Ghilbert files, but I can't seem to find a download for it. Can anyone
point me in the right direction?

[Marnix Klooster]

Op 13-07-09 03:15, Steven (sbal...@gmail.com) schreef:

> I've read mentions of a program that can convert .mm files into
> Ghilbert files, but I can't seem to find a download for it. Can anyone
> point me in the right direction?

The only thing I know of is a Python script called mm_xlat.py, and it is
in the root directory the Ghilbert darcs repository at
http://www.ghilbert.org/repo/ghilbert/ (script last updated Jan '07).

However if I recall correctly, this script was fairly specific for the
set.mm file, and it probably would need tweaking to support an
independent Metamath file, or any .mm file that includes additional
notation for that matter.

Hope this helps.

Groetjes,
<><
Marnix