Re: [isabelle] Pitfall with type-classes in Isar-Lemma format
> BTW, the thing given as arguments to the command 'by' is called "proof
> method" or just "method" in Isar terminology.
sorry for the confusion here.
> > An alternative would be to pass the lemmas as parameters to my tactic,
> > which I have already (partially) implemented
> This would indeed follow the standard convention: a method that accepts
> implicit arguments via the context also allows the same as explicit
> arguments on the spot.
For my application, it has, however, the disadvantage that the setup has
to be repeated each time I apply a method. For example, I want to
support proofs like:
notes [refine_transfer] = some lengthy setup
notes [...] = ...
shows "?c <= a"
apply (some user-specified proof of subgoal, thereby instantiating
schematics on that the rest of the proof depends)
apply (some user-specified instantiation)
When I do the setup locally for the proof method, I have to repeat it
each time I apply the method. What I really want is to do the setup for
the whole proof.
Perhaps, what I'm doing here is an abuse of the original intention of
This archive was generated by a fusion of
Pipermail (Mailman edition) and