Re: [mizar] Strong Mizar wish: linking to consider (fwd)

[Czeslaw Bylinski <bylinski@math.uwb.edu.pl>]

---------- Forwarded message ----------
Date: Mon, 18 Mar 2002 16:31:45 +0100 (CET)
From: Andrea Asperti <asperti@CS.UniBO.IT>
To: Claudio Sacerdoti Coen <sacerdot@CS.UniBO.IT>
Cc: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] Strong Mizar wish: linking to consider (fwd)


> > I
> > understood Claudio's remark as "first use some XML-format for Mizar" just
> > as Coq uses the HELM format, which I think is very reasonable.
>

Yes. I would just like to add to Claudio's description that
as soon as you agree on some DTD for Mizar and export
Mizar documents into XML, we would
be VERY interested to work on them, applying our HELM
technology and knowhow (e.g. for rendering, or for
the implementation of complex searching and retrieving
functionalities).
We do not have enough knowledge on Mizar to positively
contribute in the overall design of the DTD, but we could
probably also help in the definition of some components
of the markup.
In conclusion, we are very interested in the idea of
porting Mizar into XML, and hope it will go on.

			-- andrea asperti