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

Hi Mark,

The command print_configs shows all configurations with their current setting.
The types tell you which values are possible on the right-hand side.
E.g., for bool, values are true or false, for real and int, it could be some number, for strings you have to look further in the documentation and references.

For unification, we provide 4 configurations:

  unify_search_bound: int = 60
  unify_trace_bound: int = 50
  unify_trace_simp: bool = false
  unify_trace_types: bool = false

Setting those will probably do what you want.


On 06/18/2012 08:40 AM, 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.