3.2.1 vocabulary部

 vocabulary 部には,article の中で使われている vocabulary の登録されているvocabulary file (.VOCファイル)のファイル名を大文字で書きます. ファイル名の拡張子は省略し,複数の vocabulary file を書く場合はコンマ( , )で区切って書きます1. 行末には セミコロン( ; )を書きます.また, vocabulary 部以外もこれと同様に書きます.
 Mizar ライブラリに登録されている article で使用されている vocabulary が登録されている vocabulary file は, 1つの特殊な形式のファイルにまとめられています.
 使用する vocabulary が登録されている vocabulary file を探すには,MS-DOSのコマンドプロンプト, またはLinuxのプロンプトで

   FINDVOC [vocabulary]

とします.また, vocabulary file に登録されている vocabulary を表示するには,

   LISTVOC [vocabulary]

とします.

--------------------------
 1HIDDEN.VOC に登録されている vocabulary については, vocabulary 部に書かなくても使うことができます.