environのインポートディレクティブ

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、

1. vocabulary （単数？）
2. notation （単数？）
3. constructors
4. definitions
5. theorems
6. schemes
7. requirements

それ以外に次を確認している。

1. registrations
2. equalities
3. expansions

.logファイルから分かる情報：

• Constructorsは*.dcoから来る。
• constructorとは、M L V R K U G である。
  • M mode
  • L right bracket
  • V attribute
  • R predicate
  • K left bracket
  • U selector
  • G structure
• Requirementsは*.dreから来る。
• Registrationsは*.dcl, *.dcoから来る。
• Notationsは*.dnoから来る。
• Registrations(Identify)は*.didから来る。
• Registrations(Reduction)は*.drdから来る。
• Registrations(Properties)は*.dprから来る。
• Definitionsは*.defから来る。
• Theoremsは*.the, *.dcoから来る。
• Schemesは*.schと*.dcoから来る。

拡張子	分類
.dco	Constructors と無効（cutting off）情報
.dre	Requirements
.dcl	Registrations
.dno	Notations
.did	Registrations(Identify)
.drd	Registrations(Reduction)
.dpr	Registrations(Properties)
.def	Definitions
.the	Theorems
.sch	Schemes

すべてのディレクティブが独立なのではなくて、vocabulariesとnotationsは依存関係にあるようだ。おそらくconstructorsも依存していそう。