[isabelle] Giving a symbolic name to a tactical



Hi all,

In my proof, at several positions, there occurs a step like this:
     apply (
       (intro exI conjI),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps, (rule compress_u_a[THEN tranclp_into_rtranclp] | rule elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN tranclp_into_rtranclp] ))+,
       (rule rtranclp.intros),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps, (rule compress_u_a[THEN tranclp_into_rtranclp] | rule elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN tranclp_into_rtranclp] ))+,
       (simp add: Un_ac)
     )

And I fear this step will even get longer in the future, but it's always the same step. Is there a way to give this a symbolic name once, and then refer to the step via this symbolic name ?

If the only way of doing so should be by converting this to an ML-tactical [As indicated in Christian Urban's mail of 2007-09-03], then regard this mail as a feature request:
 A nice feature would be:

   define my_tactical = tactical_expression

   and then use:

apply my_tactical
   instead of

   apply tactical_expression



Best regards
 Peter










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