1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
Note that executing an high tactic on a set of goals may be stronger
than executing the same tactic on those goals, but once at a time
Note that executing an high tactic on a set of goals may be stronger
than executing the same tactic on those goals, but once at a time