Re: [isabelle] Telling auto to use an eisbach method

Could you please be more specific? That sounds pretty much like what auto/force/blast do anyway if you use intro/elim/dest without the (!) modifier.

Larry Paulson

> On 2 Sep 2016, at 13:25, Joachim Breitner <joachim at> wrote:
> It is not (safe) simplification that I want to
> instrument, but rather the part of auto that does proof search, i.e.
> undoes a rule application if it turned out that it did not lead
> anywhere.

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