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

Dear Larry,

Am Freitag, den 02.09.2016, 13:34 +0100 schrieb Lawrence Paulson:
> 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.

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.


Joachim Breitner
Post-Doctoral researcher

Attachment: signature.asc
Description: This is a digitally signed message part

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