HOL Light入門その２

先ほどの hol_light フォルダーにおいて，

rlwrap -r ocaml

と入力すると

        Objective Caml version 3.11.2

# 

のようにOCamelのインタープリタが起動するので，プロンプトに

#use"hol.ml";;

と（ # 記号も）入力，しばし待てば

	Camlp5 Parsing version 5.14

# 

と表示され，基本的な定理や証明ツールのロードが完了（このロードの作業は起動する毎に必要です），HOL Light の世界になります．