[isabelle] Giving a name to a tactics-expression



Hi all.
[Apologies if this question already was on this list some time ago]

Is there a way to give a short name to a complex tactic-expression. I have, e.g., the following pattern that I frequently use.
 apply (((erule (1) lemma1)+)?,erule lemma2,simp)+

Lemma1 and lemma2 are two (fixed) lemmas proven in my theory.

Instead, I would like to write something like:
   define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+
 and later:
   apply (my_method)

However, the only way I know is something like:
method_setup my_method = {* <Some scary ML-code, much more boilerplate than the above tactics-expression, and much more complicated to read and write if one does not know the ML-interface by heart> *} "..."

Is there a way without manually translating the above Tactics-expression to ML code?

Regards and thanks,
 Peter







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