R: PVS GPLed

> I once started such a manual.  My "tutorial" ("... in nine
> easy steps") was supposed to be part of it.  But no one in
> the Mizar group seemed to think it would be useful (which I
> still find very strange!), and by now I don't think I ever
> will write it. Not as long as Mizar doesn't support empty
> types, doesn't have much simpler environments, doesn't have
> binders, doesn't have the old style "from" :-)  Ah yes:
> and doesn't support "then" after "consider".

> Freek

I think you tutorial is very useful (I have read it), and I put the
link to this tutorial on Mizar Wiki site: http://wiki.mizar.org about
two years ago.
It seems that new Mizar users simply doesn't aware of the existence of Mizar
Wiki and your tutorial.
Two years ago I tried to understand Mizar at low level, because I
like to understand how the things work. I still think it is possible
to create an alternative implementation of Mizar language, though
now I am a happy user of Isabelle system.

By the way, what do you mean by 'old style "from"'?

Michael Nedzelsky