Hi Freek, > Would you think a version of Mizar that only would report the > _first_ non *4 error and then quit, that it would be much > less usable than the current one? How about proof sketches? - I like the "top down" approach when writing articles very much. Josef