Piotr: >Winning in error recovery is like winning in any other >guessing game. And the winning strategy is: stay away. I'm not sure. I _like_ the error recovery in Mizar, even if I'm not sure how important it is. Maybe a very basic error recovery strategy (skip to the next "theorem" or "definition" keyword) would go a long way with a fraction of the effort. I don't know. Freek