[mizar] XML DTD for Mizar articles?

[Freek Wiedijk <freek@cs.kun.nl>]

Hello,

A question that occurred to me because of a discussion with
Andrea Asperti from the MoWGLI project (Nijmegen is part of
this project, which is about putting mathematics -- including
formal mathematics -- on the Web):

Has someone already defined a proper XML DTD for Mizar
articles?  if so: can that someone show this DTD on the Mizar
forum?  I'm very curious what it looks like, especially the
encoding of the proof steps.

If not: shouldn't we have one?

Czeslaw told me at Calculemus that the Mizar people were
considering writing an XML export tool for Mizar.  But a DTD
would be an essential prerequisite for this, so I wondered
whether that already had been done.

Freek