HOL4 のインストールスクリプトは http://d.hatena.ne.jp/ehito/20130219/1361260859 に書きましたが,システムとして HOL Light と大きく異なる点を幾つか述べます. まず,ライブラリーのロードとオープンについてです. デフォルトでの起動では,例えば - Induct; > val it = fn : term list * term -> (term list * term) list * (thm list -> thm) は良くても - INDUCT_TAC; ! Toplevel input: ! INDUCT_TAC; ! ^^^^^^^^^^ ! Unbound value identifier: INDUCT_TAC のように知らぬ素振です.ところが help で尋ねると - help"INDUCT_TAC"; -----