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