[isabelle] Enabling unification tracing in Isabelle/jEdit.



Hello,

I am using Isabelle/jEdit. I infer from the tutorial that when using
ProofGeneral there is a "Isabelle --> Settings" menu. Is there an
equivalent way of accessing/changing these settings when using jEdit? I am
happy to write lines like

using [[simp_trace=true]]

into my thy file on a temporary basis. I see the 'Tracing' toggle on the
jEdit GUI but assume this is to control general viewing of trace output; I
still need to enable specific tracing.

Is there a list of what possible values for X and Y are possible in lines
like

using [[ X = Y ]]

In particular I would like to enable unification tracing.

Cheers

Mark




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.