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.

Kind regards,
Tjark







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