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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and