Re: [isabelle] Changing unification depth

On Fri, 26 Nov 2010, John Munroe wrote:

theory Test
imports Complex_Main

declare [[unification_search_bound = 70]]

It seems that Unify.search_bound is fixed to the value of
Unify.search_bound_value, which is default to 60 due to

Did you really try it as above? The configuration option is called "unify_search_bound". Here is an example in Isabelle2009-2:

  declare [[unify_search_bound = 70]]

  ML {* Config.get_global @{theory} Unify.search_bound *}
  ML {* Config.get @{context} Unify.search_bound *}

For historical reasons there is a snag: unify options can only be modified in a global context. E.g. consider:

  lemma A
    using [[unify_search_bound = 42]]

  ### Ignoring local change of global option "unify_search_bound"

As usual in Proof General, such warnings are easily overlooked. As usual, it will be much more visible in the Isabelle/jEdit prover IDE, although I've already had some complaints that warnings are too prominent there.


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