Hi Freek, Freek Wiedijk wrote:
We teach courses for freshmen. The environment is fixed. Incremeted if necessary. And it is customized, we do not use MML at all.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.
Greetungs, Andrzej