私の環境

　今回は私がHOL Lightで証明を書く際の環境？をご紹介します．
　OSはWindows，エディターは秀丸，OcamlはDOS窓内です．
　秀丸はシェアウエアですが，軽快な作動と柔軟なカスタマイズ性，Cライクなマクロが特徴で，私は例えば，カーソルのある論理行をクリップボードにコピー，カーソルを次の行の先頭へ移動といったマクロをCtrl＋Tabにバインドしたり，g，e関数で書いた対話的証明をproveに書き換えるマクロなどを組んでいます．

　WindowsのOcamlには独自のGUIが附属していますが使い辛いので，DOS窓でocamlを実行しています．Unixのocamlではコマンド編集に，rlwrap ocamlのような工夫が入用ですが，WindowsではOcamlのtoplevel loopでもDOS窓デフォルトのコマンド履歴などが使えます．例えば，矢印キーによる履歴参照は勿論ですが，F8によるコンプリーションは，秀丸のAlt+Enterによる単語補完と同様至便です．また，クリップボードからのペーストは，ウインド内の任意の位置での右クリックのみで実行され，HOL Lightのコードを対話的に実行するのに最適です．

　フォントが大きめなのは私の視力のせいです（泣）．
　なお，emacsのProof Generalは試験的な実装ですが，http://weyl.math.pitt.edu/hanoi2009/Software/HOLLightMode のHOL Light modeは画面が大きければ使い易いかも知れません．