[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.