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 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
> anywhere.





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