# [isabelle] tactical combinators

Hi all,
I'm trying to write the (recursive) tactic described as below:

`A - apply some elimination rule to the subgoal n producing 3 subgoals
``(n, n+1, n+2), then :
`` 1 - simultaneously apply some elimination rules to the 3
``subgoals. then
`` 2 - apply the same tactic to the 3 subgoals (with different
``parameters for each case).
`

`My problem is that when applying the elimination rules in 1, this can
``lead to 0 or more subgoals,
`so I cannot apply the tactics in 2 to the subgoals (n, n+1, n+2).

`My question is: Wich combinator should I use in step 1 and 2 in order to
``apply (locally) these steps with rules (n, n+1, n+2) whatever the result
``of applying the rule 1.
`
Thanks a lot,
Abdou

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