How to enable "Tracing" in Isabelle/jEdit

Question

I'm a vim fan, but only emacs has this Isabelle/HOL environment. jEdit is great, but I cannot use

using [[simp_trace=true]]

like in emacs.

How to enable "Tracing" in jEdit?

Answer 1

You can indeed use simp_trace in the middle of a proof in Isabelle/jEdit, like so:

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

Alternatively, you can declare it globally, like so:

declare [[simp_trace]]

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

Both give you the simplifier's trace in the "Output" window when your cursor is just after the apply simp statement in jEdit.

Answer 2

If you need a trace depth deeper than 1 (default), you fine-tune it by

declare [[simp_trace_depth_limit=4]] 

This example then gives a trace depth of 4.