Re: [mizar] Strong Mizar wish: linking to consider

[Claudio Sacerdoti Coen <sacerdot@CS.UniBO.IT>]

> > If we do the XML export in some finite time, a pretty printer will be 
> > just a style sheet.

> A postprocessor for formatting Mizar texts is needed to convert Mizar
> texts to some standard presentation style - I see it as a substantial
> automated reediting of Mizar text rather than just XML style sheet.

 Hi,

 in case you are interested in exporting to XML and use stylesheets
 or other machinery to pretty-print the text (and make it more interactive),
 can I please suggest you to have a look at the forthcoming european
 IST project MOWGLI (http://mowgli.cs.unibo.it) and to the still active HELM
 project (http://www.cs.unibo.it/helm) that does something similar for
 Coq proofs. Note that substantial automated reediting of Coq lambda-terms
 is done using "just" XML style sheets (i.e. several thousands lines of
 XSLT).

					Regards,
					 C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://caristudenti.cs.unibo.it/~sacerdot
----------------------------------------------------------------