Re: [isabelle] Surprises with transfer method
On Do, 2013-01-31 at 10:58 +0100, Florian Haftmann wrote:
> When experimenting with lifting and transfer, I ran into situations
> where transfer yields funny goal states. I have distilled two prominent
> candidates into the attached theories. The first one seems to me a
> result of erroneous backtracking in a tactic behind the transfer method.
> For the second one, I am standing in the dark
Not being an expert on the impl of transfer, the second one looks like
an artifact of a higher-order unification, where one intended a
first-order matching ...
> Maybe experts on transfer can comment on this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and