HOL Light Tutorial

　突然（でもないかも？）ですが，今回からしばらく，HOL Lightについて少し詳しく書いて行きたいと思います．

　まず，インストールですが，前回の方法は，手軽とはいえ

HOL Light 2.20,
built 22 December 2006 on OCaml 3.09.3

という古い安定化バージョンであり，パッケージ数も多くありません．本家のサイト
http://www.cl.cam.ac.uk/~jrh13/hol-light/
の案内の通り，現在は
http://code.google.com/p/hol-light/
から逐次更新されるソースを参照できる他
http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.zip
という２０１０年１月１０日付の

version2.20++

も公開されており，ここではこのセットを軸にお話します．