7.4.4 Useful Command

There is a useful batch command named MIZF.BAT and when the following form takes place, it checks to see if there is any need for accommodation. When there is a need, it carries out the accommodation first and then the Mizar checker is executed.


When there are more errors, it enters the error numbers in the form of a comment to an article. At the end of an article, risen error numbers and messages are entered into a comparison table (entered comments are erased at the time when MIZF command is executed next).