[isabelle] Unifier trace in solve_direct
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?
If I have identified the lemma, how can I exclude it from solve_direct?
Thanks in advance for any hints,
This archive was generated by a fusion of
Pipermail (Mailman edition) and