Re: [isabelle] Giving a name to a tactics-expression



Peter Lammich schrieb:
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)+

Trying to translate it to ML, I cannot find any ML-tactics equivalent for "erule (1)". There is only etac, but this seems to have no number of additional premises.

Regards & Thanks,
 Peter

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.