証明メソッド

1. proof method周辺 - 檜山正幸のキマイラ飼育記 メモ編

isar-refの"Chapter 7 Proof scripts"あたりに書いてある。

1. セオリーのトップレベルで使うキーワードはセオリーコマンド
2. theoremなどのゴール提示コマンで証明モード（リーズニングモード）に入る。
3. 証明モード内で使うコマンドが証明コマンド、タクティク適用のapply、バックトラック／リトライに使うback など。
4. done, by, oops, sorryなどで証明モードを抜ける。基本的に、責務を果たさないと抜けられない。
5. applyはタクティクを実行する。
6. タクティクと証明メソッドは同義のようだ。
7. タクティクの引数がある。証明コマンドの引数にタクティク、タクティクの引数、という入れ子構造。
8. ruleタクティクの引数はルールと呼ぶ。
9. ruleタクティクは、旧名resolve_tac、分かりやすかった。
10. ruleタクティクの引数はルール名だが、このときのルールは定理。なぜなら、オブジェクト論理のルールはメタ定理だから。