Isabelle には、quick_and_dirty
でプルーフをスキップできるモードがありますsorry
。jEdit ではデフォルトで有効になっており、デフォルトでは無効になっていますisabelle build
。設定を変更するにはどうすればよいですか
- jEdit で (対話的に、またはコマンド ライン パラメーターを使用して)、
- の場合
isabelle build
、コマンド ラインから、 - について
isabelle build
は、ROOT
ファイル内にそれぞれ。
また、Isabelle に、できれば jEdit でインタラクティブに、「現在の理論とその親のどの補題がsorry
"を使用して証明されているか?
(Googleで見つけたメーリングリストの投稿とは対照的に、常に最新の回答があることを期待して、ここでこれを尋ねています。)