Re: [isabelle] Strange simplifier behaviour



On Wed, 1 Apr 2015, 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. Is there some kind of workaround?

The isar-ref manual section "9.3.2 Declaring rules" provides a specification of "simp" rules. There are also some explicit examples of HO things that don't work, by the very construction of all this.


	Makarius




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