Isabelleのチュートリアルを読みながらまとめていきたいと思います。 http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf 最新バージョンはIsabelle2009-1。バージョンが変わる前に最後までいけたらよいなと。 環境はMac(Snow Leopard)にMacPortsでIsabelleとProof Generalをインストールし、Carbon Emacsで動かしています。X-Symbolは使用していません。