isabelle - Isabelle/jEdit で「トレース」を有効にする方法

Question

私はvimのファンですが、この Isabelle/HOL 環境を備えているのはemacsだけです。jEditは素晴らしいですが、私は使用できません

using [[simp_trace=true]]

emacsのように。

jEditで「トレース」を有効にする方法は?

Answer 1

simp_trace次のように、Isabelle/jEdit で証明の途中で実際に使用できます。

lemma "(2 :: nat) + 2 = 4"
  using [[simp_trace]]
  apply simp
  done

または、次のようにグローバルに宣言することもできます。

declare [[simp_trace]]

lemma "(2 :: nat) + 2 = 4"
  apply simp
  done

apply simpどちらも、カーソルがjEditのステートメントの直後にあるときに、「出力」ウィンドウに簡略化のトレースを表示します。