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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and