Re: [isabelle] Unifier trace in solve_direct



On 31.07.2014 09:42, Peter Lammich wrote:
> Hi List,
>
> when I type solve_direct, it outputs a lot of unifier trace messages
> "Enter MATCH" and "unification bound exceeded". 
>
> I think it is due to some lemma that I have proven, and that hapens to
> have an unfortunately shaped conclusion.
>
> How can I identify the lemma? Is there any general method?
solve_direct basically calls "find_theorems solves", which again tries
to solve the current goal with several tactics applied to "all"
theorems. Your best bet is to dive into the implementation of
Find_Theorems.filter_solves.
> If I have identified the lemma, how can I exclude it from solve_direct?
You cannot. Except with concealing the lemma from the available fact
space, which is probably not what you want.

  -- Lars




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