Re: [isabelle] Odd failure to match local statement with pending goal.

I'm afraid I can't. In general, the name of a bound variable should be irrelevant. I considered the possibility of a hidden effect on type inference, but all variables have the same type, namely tree.


Larry Paulson

On 27 Jul 2011, at 12:21, Bertram Felgenhauer wrote:

> The failure disappears if I rename the r'a to r'a' inside the existential
> quantifier of the conclusion (included as a comment in the attachment),
> i.e., simply by doing an alpha conversion. I find this very odd. Can
> anybody explain this behaviour?

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