IsabellをML開発環境として使う手順

• 参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編

1. デスクトップにIsabelle2016（少し古い）のアイコンがある。
2. このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。
3. Isabelle2016.exeの実体は、jEditをフロント、PolyMLをバックとするシステム。
4. jEditはマルチタブエディタなので、とりあえず新規文書を作る。
5. この文書をthyファイルとしたい。
6. ファイル名拡張子が .thy でないとthyファイルとは認識されない。
7. Hoge.thy という名でいったんセーブする。
8. theory Hoge[改行]imports Pure[改行]begin[改行] と書く。
9. theory名は、ファイルのベース名と一致しないとダメ。imports宣言は必須。
10. fuga.ML という名のファイルを用意する。PolyMLの拡張子は大文字で .ML 。
11. thyファイルに ML_file "fuga.ML" という行を加える。
12. fuga.MLを開く。
13. 以上で、MLの開発環境が出来上がり。