Re: [mizar] the Why project

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

Dear Andrzej,

>Who is interested in the Why project, and who did the Mizar
>stuff for Why?

I am very much interested in Why, although I never really did
something with it.

The Mizar output was added by Jean-Christophe after he had
told me that it was not much work to add output for another
prover.  I don't remember the details, but I think there was a
little article that was needed to support the Mizar code that
was generated by Why.  If so, it is probably part of the Why
distribution.  Jean-Christophe wanted to install that article
into the MML directory when installing Why.  I told him that
that was not the proper thing to do, but we never submitted
this (tiny) article to MML either.

So it would be interesting to know whether the Mizar output
from Why still works with the current version of Mizar.  I
doubt it, really.

Freek