isabelle - 如何在 Isabelle/jEdit 中启用 "Tracing"

Question

我是 vim 的粉丝，但只有 emacs 有这个 Isabelle/HOL 环境。 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 中的声明。