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.
> On 2 Sep 2016, at 13:25, Joachim Breitner <joachim at cis.upenn.edu> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and