Re: [mizar] Private DB

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

Hi Josef,

>So yes, whatever is the mechanism deciding about Mizar
>changes (I strongly suspect that the mechanism is _you_ :-)

Which is the way it should be.  Mizar is a such a great system
exactly because of this.  It gives a unity to the system, and
prevents it from "diverging".

>Freek's tutorial

My original plan was to write a book about Mizar, together
with Andrzej, consisting of four parts: a tutorial, a history
of the system, a manual of the language, and a manual of the
programs.  I never got beyond the tutorial, though.  Maybe I
should go to Poland for a month and write the two manual
parts.  (And then forget about the history part :-))

If you want to point to the tutorial, please tell me, so I can
put it in a reasonable place.  Currently the most recent
version is in the directory of my proof assistants course,
which is not where one should link to.

Freek