Hi Josef, >> 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? The definition of a FPS (formal proof sketch) is that it only has *4 errors :-) Freek