Sorry for the noise, I overlooked the "non" in "_first_ non *4 error". Josef On Wed, 4 Feb 2004, Josef Urban wrote: > > 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 >