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.
Is there some kind of workaround? Cheers, Manuel
Description: S/MIME Cryptographic Signature