3.2.1　Vocabulary Section

In the vocabulary section, we write the names of the vocabulary files (.VOC file) that are registered and used in articles with capital letters. We omit the extension unit of a file name, and when writing many vocabulary files, we write by using commas (for vocabularies that are registered in HIDDEN.VOC, we can use them without writing them in the vocabulary section). At the end of sentences, we write semicolons. Also, we write the same way with places other than the vocabulary section.
    The vocabulary file that has registered vocabularies that are used in an article registered in the Mizar library is summed up in a special file.
   To look for the vocabulary file that has registered vocabularies that we want to use, we type the following at the command prompt of MS-DOS, or the prompt of Linux.

      FINDVOC [vocabulary]

Also, when we want to indicate vocabularies that are registered in the vocabulary file, we type the following.

     LISTVOC [vocabulary]