環境部では，引用する形式の書かれているファイル名を書きます。
 ::環境設定
 environ 
 ::--------------------------------------------------------------------------------------
 ::語彙、単語集（+,-,*,/,exp(),log(),...）
 :: 対象・作用を表す用語を記しているファイル
  vocabularies ARYTM, ARYTM_3, RELAT_1, ARYTM_1, ABSVALUE, SQUARE_1, XCMPLX_0, COMPLEX1, POLYEQ_3;
 ::--------------------------------------------------------------------------------------
 ::記号の作用範囲（整数+整数,実数+整数,...）
 :: 対象・作用を表現するかを表しているファイル
  notations TARSKI, SUBSET_1, ORDINAL1,NUMBERS,XCMPLX_0,XREAL_0,ABSVALUE, SQUARE_1,POLYEQ_3;
 ::--------------------------------------------------------------------------------------
 ::生成子、構築（「整数:整数+整数」,「実数:実数+整数」,...）
 :: 概念間の階層構造等の関係を記述したファイル
  constructors REAL_1, ABSVALUE, XCMPLX_0, XREAL_0, XBOOLE_0,SQUARE_1,POLYEQ_3;
 ::--------------------------------------------------------------------------------------
 ::同要素の集合体、群
  registrations XREAL_0, REAL_1, NUMBERS, ARYTM_3, ZFMISC_1, XBOOLE_0, XCMPLX_0;
 ::--------------------------------------------------------------------------------------
 ::条件範囲(集)「整数:{0,1,2,3,...}」,「実数:-∞より上、∞未満」,「ブール:0,1」,...
  requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 ::--------------------------------------------------------------------------------------
 ::定義(集)
  definitions TARSKI, REAL_1, XREAL_0;
 ::--------------------------------------------------------------------------------------
 ::定理(集)ファイル
  theorems AXIOMS, REAL_1, ABSVALUE, XREAL_0, XCMPLX_0, XCMPLX_1;
 ::--------------------------------------------------------------------------------------
 ::公理図式（A→B,￢A∨B,...）
  schemes FRAENKEL, BINOP_1, SUBSET_1;
証明の型(まずはmodeで探してみる)
--------------------------------------------------------------------------------------
[http://markun.cs.shinshu-u.ac.jp/mizar/lib.htm ライブラリーファイル一覧]