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

我是vim爱好者，但只有emacs具有此Isabelle/HOL环境。 jEdit很棒，但是我不能使用

using [[simp_trace=true]]

就像在emacs中一样。

如何在jEdit中启用“跟踪”？

最佳答案

实际上，您可以在Isabelle/jEdit的证明中间使用simp_trace，如下所示:

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

或者，您可以全局声明它，如下所示:

declare [[simp_trace]]

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

当您的光标位于jEdit中的apply simp语句之后时，两者都将在“输出”窗口中提供简化程序的跟踪。

关于isabelle - 如何在Isabelle/jEdit中启用 “Tracing”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/19018023/