Re: [isabelle] Converting apply-style induction to Structured Isar
On Fri, 2011-04-01 at 10:09 +1100, Rafal Kolanski wrote:
> The "cons_rewrite" lemma is in direct conflict with app.simps, so they
> can't both be in the simpset at the same time.
I've found metis quite handy in similar situations. metis knows about
symmetry, so (unlike simp) it may still succeed when equalities are
oriented the wrong way.
This archive was generated by a fusion of
Pipermail (Mailman edition) and