Hi Andrzej, >So, I thnik we need regular Mizar cources, like in UwB. I teach a Mizar course each year in Nijmegen, as part of my course "proof assistants". The few students that I have seem to like the course, but even so they are not able to get the environment right by themselves, even when they start by copying it from an old article. Freek