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.
> 
> Cheers,
> 	Florian
> 







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