Re: [mizar] quite some questions about functions

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Tue, 13 May 2008, Jesse Alama wrote:

> Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
> > If it is a new article (not yet in MML), either use the method Adam
> > described, or you can also paste the article into
> > http://octopi.mizar.org/~mptp/MizAR.html and press the Send button.
>
> What's going on at octopi.mizar.org?

It is a fairly experimental service for explaining Mizar atomic 
inferences (and doing more) using automated provers. As a byproduct, it 
also html-izes articles. More at 
http://mizar.uwb.edu.pl/forum/archive/0804/msg00004.html .

Josef