7.2 Preparation for Using Mizar
To use Mizar, we first need to make our own directory.
Here, we explaine an example according to a MS-DOS version. In C:\, a directory named USER needs to be created and our own directory is made
under it. For instance, because my name is Nakamura, we need to make a
directory named nakamura under the USER directory. Below it, three directories
of TEXT,DICT,and PREL are created.
To explain each directory: TEXT directory is for placing
Mizar articles (.MIZ file) that the users write. In addition, an intermediate
file that outputs the Mizar system is also placed here. DICT is an abbreviation
of DICTionary and the vocabulary file (.VOC file) that the user has written
is placed. New words are written under this vocabulary file. PREL is an
abbreviation of PRELiminaries, and this is used to store the necessary
files to view articles that are not registered in the Mizar library.
Usually, when using Mizar, we assume that a current directory is one's own directory under C:\USER. For example, when using the command of Mizar called accom which we explain by 7.4.1, we enter it as follows.
C:\USER\NAKAMURA\ACCOM TEXT\EXAMPLE1.MIZ
C:\USER\NAKAMURA\TEXT \DICT \PREL |