先に関連URLs：
- HOL : http://hol.sourceforge.net/
- Moscow ML : http://www.dina.kvl.dk/~sestoft/mosml.html
- Prosper : http://www.dcs.gla.ac.uk/prosper/toolkit/
- Isabelle : http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
- SML of New Jersey : http://www.smlnj.org/
- Proof General : http://proofgeneral.inf.ed.ac.uk/
- CygWin : http://www.cygwin.com/
- MinGW : http://www.mingw.org/
- Borland C++ Compiler 5.5.1 : http://www.borland.co.jp/cppbuilder/freecompiler/index.html
Windows（Thinkpad X31）でHOLを動かしたくなった。
以前はWindows用バイナリが提供されていたらしい。今はないので、手動でインストールを試みる。ざっと見、Cコンパイラとmakeが必要そうだが、かまわずやってみる。とりあえず、…動かない。
Cで書かれたライブラリを無視するようにすればいいような気がするのだが、完全にインストールしたほうがいいのだろう、やっぱり。.c以外に、.y、.lexなんてのがあるから、cc, make, yacc, lex相当品は必要そうだ。
IsabelleならCygwinで動くようだ（→http://www.abo.fi/~vpreotea/isabelle/）。が、Prosper経由で動かしたいので、HOLにこだわってみよう。選択肢としては：
Windowsの.exeと.dllだけで話が済めばいいのだけど、.soなんてファイルがあるんだよな。なにこれ？ やだなー。
それにしても、Moscow MLってナカナカだなぁ。バイトコードコンパイラ付きで、ランタイムエンジンとリンクして.exeが作れる（配布可能か？）。
