Re: [isabelle] Strange simplifier behaviour

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

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.


Is there
some kind of workaround?



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

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