問題タブ [isar]

シンボルや補題の定義に直行できるショートカットやコマンドが存在します。(Emacs の GTAGS の「ALT+」のように)

IDEで検索コマンドを実行する必要があるCoqのものとは対照的に（ただ私見ですが）非常に便利です。

jEdit に基づく標準の Isabelle IDE で定義を検索するには、どのキーの組み合わせを押せばよいか忘れてしまいます。

思い出していただけますか？

Modus Ponens のそのようなバリアントがあると仮定しましょう

定理の証明に適用できますか? (つまり、A:=A、B:=A、および A-->A を以前に証明されたかのように使用します)

そうでない場合、なぜですか？この定理を証明する他の方法をいくつか知っています (「仮定を適用する」またはフレーゲの命題計算公理からの 5 段階証明) が、証明力学のこのニュアンスに興味がありました。

1 つのルールがありますが、別の [許容される] ルールを取得したいのですが、何が問題ですか?

Isabelle/Isar でルール導入を行いたい。見つけた

また

私がやりたいことを正確に行います。しかし、「新しいスタイル」の Isar を使用してその行を書くにはどうすればよいでしょうか? ご覧のとおりP、関数の誘導規則で変数をインスタンス化する方法を Isabelle に伝えようとしているだけですf。