Re: [mizar] Private DB

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Hi Josef,

Josef Urban wrote:

> That's exactly the point. Mizar is very good at discouraging newbies. 
> And with arguments like "we have more important work to do, than to 
> add simple features for newbies" it will hardly change.
I am not against "simple features for newbies". I guess you work on it.

On the other hand I wonder what "newbies' means. I almost believe that 
it is a bad practice just to get a student and order him "formalize this 
and this". So, I thnik we need regular Mizar cources, like in UwB. I am 
very upset that preparing the simplest Internet course "Binary 
Relations" failed. I do not want report who promised to prepare it :-).

Reagrds,
Andrzej