Re: [isabelle] Enabling unification tracing in Isabelle/jEdit.

Dear Mark,

in Isabelle2012 it is not possible to change configuration options via jEdit menus. Concerning the question where available configuration options are to be found: The most comprehensive "official" reference (besides the sources) is the Isabelle Reference Manual (open via 'isabelle doc isar-ref' from a command line). Another alternative is the command


I'm not aware of an option for tracing unification (which does not mean that such an option does not exist, I just don't know).



On 06/18/2012 03:40 PM, Mark Wassell wrote:

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

using [[ X = Y ]]

In particular I would like to enable unification tracing.



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