Hi Michael,
About using XML files produced by the Mizar: All my Mizar related work will be in public domain, hence the question: May I freely use these files? Are there any licensing problems?
I guess their licence would be the same as that of the Mizar articles distributed in MML. Don't ask me what that licence is, I don't know, and I wish that Association of Mizar Users clarified this.
On the other hand, I also think that having Mizar rewritten in a high-level language like OCaml would be useful.My first goal is to create the working parser. I assume it will take 2-3 months.
It also depends on what is exactly meant by "parser". E.g. the type analysis and disambiguation of overloading is in Mizar done in a separate second pass (called "Analyzer").
Josef