Re: [isabelle] Strange simplifier behaviour




On 01/04/2015 16:56, Manuel Eberl wrote:
Hallo,

I found that the simplifier fails to apply certain simplification rules
when I would have expected it to. This occurs both in the development
version and Isabelle 2014. (see attachment)

I suspect it has something to do with higher-order unification.

HO Matching. The simplifier only works reliably with *higher-order patterns* on the left-hand side: free variables may only be applied to distinct bound variables.

Tobias

Is there
some kind of workaround?

Cheers,

Manuel


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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