前回紹介したライブラリーのロード，オープン以外にも，グローバル変数の設定や，自作の定理，tacticなどを起動時に読み込ませるには，ホームディレクトリ（WindowsではC:\Users\ユーザー名）にhol-config.sml hol-config.ML .hol-config .hol-config.sml .h…

HOL4 のインストールスクリプトは http://d.hatena.ne.jp/ehito/20130219/1361260859 に書きましたが，システムとして HOL Light と大きく異なる点を幾つか述べます．まず，ライブラリーのロードとオープンについてです．デフォルトでの起動では，例えば - I…