After checking for all the improvements in an article, ENV is exectured next. When ENV is executed, one needs to accommodate it. Then, the file for referring that article is made from one's article (.MIZ file). When MIZ2ABS is executed, only +Theorem and Definition are picked out to make the abstract file (.ABS file). In addition, when PRE is executed to make that article referable, it copies the necessary file into one's directory.
Command used after revision
ENV Makes files for reference.
MIZ2ABS Makes abstract files.
PRE Copies files so that the article can be seen.
In addition, when the article is cited, names of authors, their unit, their address, and references are written in normal sentences and made into a .BIB file. Please use bibart.exe exclusively as an input tool.
The article is created with the process above and is sent to the Mizar Society on a floppy disk. If this article is good enough, it will be accepted and an acceptance notice will be sent. When it is accepted, it will be automatically translated into English and will be published in the Formalized Mathematics magazine (it may not be accepted).