教育的証明ドキュメントの書き方

「なるほど」とは思うが、なんか、これしか方法がないのかよ？ とも感じる。

1. Isabelleではgoal文はないので、lemma "命題" と書いて、この行の表示（カーソルあわせてOutputを見る）で、ゴールを見せる。
2. タクティクの説明は、apply(タクティク) oops とする。
3. つまり、lemma "ゴールの例" apply(タクティク) oops でゴールとタクティクとサブゴールズを説明する。
4. thmでルールベース＝定理ベースの内容を見せる、複数のルールを一度に見せることもできる。
5. Isar statement format でルールベース＝定理ベースの中身を表示するには print_statementを使う。
6. textで説明を加える。
7. 練習問題は、lemma 名前や番号: "命題" oops として書く。
8. section subsectionなどで文書構造を作る。

こうやって出来た教育用のドキュメントは、「人が読む」という目的のドキュメントじゃないよね。単にIsabelle/jEditのためのスクリプト。カーソル移動しながらOutputパネルを見る行為をしないと何も分からない。