如何在 Isabelle/jEdit 中启用“跟踪”

I'm a vim风扇，但仅emacs有这个 Isabelle/HOL 环境。jEdit很棒，但我不能使用

using [[simp_trace=true]]

like in emacs.

如何启用“跟踪”jEdit?

你确实可以使用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 simpjEdit.h 中的语句