Re: R: [mizar] PVS GPLed

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

Dear Michael,

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

Nowadays to use a scheme you need to define predicates
and/or functors that match the arguments of the scheme using
"defpred" and "deffunc".  Mizar used to be able to figure
out by itself what the instantiations of the predicates and
functors in the scheme were just by looking at the shape
of the formulas.  I liked it that way.

I'm sure that sometimes it was ambiguous, and that the
implementation of _how_ it worked was a big mess.  But in
practice it worked well for me, and I miss my proof looking
clean, without all the "defpred" noise.  When presenting
Mizar in a talk this is often one of the things that makes
my examples less convincing.

Freek