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



Possibly you could accomplish what you want using a âwrapperâ. Unfortunately, they are very obscure. See The Isabelle/Isar Reference Manual, section 9.4.7, Modifying the search step.

Larry Paulson


> On 2 Sep 2016, at 13:42, Joachim Breitner <joachim at cis.upenn.edu> wrote:
> 
> precisely â but auto (AFAIK) can only invoke _rules_, not _methods_.  I
> want it to invoke a (custom eisbach-defined) method in this way.
> 
> 
> The introduction rule in my example requires picking a âsufficiently
> freshâ variable, by specifying a set of variables to avoid. Such an
> intro rule does not work well with "auto", as it would leave a
> schematic variable around.
> 
> But almost always, this set of variables can be calculated from the
> context, i.e. the current goal statement. I (more or less) have a
> method that does that, and I want auto to try that.





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