で，インストール
ですが，ユーザーの多さを鑑み，Windowsの場合をお話します（コマンドやパッケージによっては外部プログラムやソースの書き換えが必要になりますが，それは逐次述べます）．
まず，HOL Lightは，Objective Caml上のプログラムなので
http://caml.inria.fr/pub/distrib/ocaml-3.09/ocaml-3.09.3-win-msvc.exe
をダウンロード，実行して表示される指示に従いOCamlをインストールします．ここでは
C:\Program Files\Objective Caml\
にインストールしたとします．
次に，HOL Light本体
http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.zip
をダウンロード，例えば
C:\Program Files\
において展開すると
C:\Program Files\hol_light\
というディレクトリが出来，そこに2200個（最新のサブバージョンでは2700個）程のファイルが展開されます．
後は，DOS窓で
cd C:\Program Files\hol_light\
set PATH=%PATH%;"C:\Program Files\Objective Caml\bin"
set OCAMLLIB=C:\Program Files\Objective Caml\lib
ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml
と入力すれば
Objective Caml version 3.09.0
#
のようにOCamlが起動しますので，プロンプトに対して
#use "hol.ml";;
と入力する（#記号も入力する）と，HOL Lightのメインパッケージがロードされます．ロードにはそれなりに時間が掛かりますが，しばらく待てば
Camlp4 Parsing version 3.09.0
#
に至り，準備完了です．
次回からは，HOL Lightの驚くべき能力をご紹介して参ります．
